[opentheory-users] Isabelle OpenTheory importer

Joe Hurd joe at gilith.com
Wed Mar 28 04:44:58 UTC 2012


Hi Brian,

I've just had chance to clone and take a look at your Isabelle
importer. Thanks for making it available, and especially for the great
NOTES file describing the challenges in integrating Isabelle and
OpenTheory. All of the higher order logic theorem provers have their
own conventions beyond the bare minimum implemented by OpenTheory, but
Isabelle is a particularly interesting case in that it goes beyond
this with logical extensions too.

Cheers,

Joe

On Wed, Jan 18, 2012 at 6:19 AM, Brian Huffman <huffman at in.tum.de> wrote:
> A mercurial repository with my OpenTheory importer for Isabelle is
> available online:
>
> http://www4.in.tum.de/~huffman/cgi-bin/repos.cgi/OpenTheory
>
> You should be able to use "hg clone" with the same url to download a
> copy of everything.
>
> The importer is tested with Isabelle version 2011-1.
>
> - Brian
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list



More information about the opentheory-users mailing list