[opentheory-users] Scalable LCF-style proof translation

[Ramana Kumar]

On Mon, Aug 5, 2013 at 11:49 PM, Alexander Krauss <krauss at in.tum.de> wrote:

>
> The opentheory tool post-processes articles extracted from theorem
>> provers, for compression and neatness purposes. To that end it does
>> both of the things you call out.
>>
>
> Which command do I have to run to get this?
>

Install opentheory as per
http://www.gilith.com/software/opentheory/install.html.
Then run it like:
  opentheory info --article --output processed.art input.art
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20130806/14b98aa8/attachment-0001.html>