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

[Rob Arthan]

Joe,

Thanks!

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.

Regards,

Rob.

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