[opentheory-users] Isabelle OpenTheory importer

[Joe Hurd]

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