[opentheory-users] Problems with the hol light Open Theory support

Rob Arthan rda at lemma-one.com
Thu Aug 1 09:03:03 UTC 2013



On 31 Jul 2013, at 21:59, Joe Leslie-Hurd wrote:

> ...
> To export a single theory from the proof logging fork of HOL Light,
> follow the instructions at
> http://www.gilith.com/research/opentheory/faq.html#export-from-hol-light
That's very useful. Are there any analogous instructions for exporting from HOL4?

> The initial start_logging command is used to switch on proof logging,
> which is off by default since most users don't want to export the
> whole standard theory library.
> However, that may indeed be exactly what you want, in which case carry
> out the following two steps:
> cd opentheory
> make theories

At the moment, I am collecting test data, so the more the merrier.

> Then you should see a lot of stuff pile up in opentheory/articles/

It did. Thanks again.



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20130801/87959ad9/attachment.html>

More information about the opentheory-users mailing list