[opentheory-users] generating proof articles

Joe Hurd joe at gilith.com
Mon Sep 5 19:37:47 UTC 2011

Hi Ramana,

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


to include instructions which reflect the current practice.



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

More information about the opentheory-users mailing list