[opentheory-users] Scalable LCF-style proof translation

Ramana Kumar ramana at member.fsf.org
Tue Aug 6 00:02:10 UTC 2013

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
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>

More information about the opentheory-users mailing list