[opentheory-users] generating proof articles

[Joe Hurd]

Hi Ramana,

Yes, these instructions are out of date and are missing details of the
export_thm command. I've updated the documentation at

http://www.gilith.com/software/opentheory/faq.html

to include instructions which reflect the current practice.

Cheers,

Joe

On Fri, Sep 2, 2011 at 2:02 PM, Ramana Kumar <ramana.kumar at gmail.com> wrote:
> The answer to "How can I generate a proof article file from a HOL
> Light theory file?" at
> http://www.gilith.com/software/opentheory/faq.html doesn't mention the
> function "export_thm". Should it?
>
> (I can't get HOL Light to build at the moment, else I would have just
> tried following the steps to see.)
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>