[opentheory-users] Scalable LCF-style proof translation
krauss at in.tum.de
Mon Aug 5 22:49:37 UTC 2013
Hi Joe, Hi Ramana,
>> - I wonder which of the offline processing that we do currently is actually
>> done similarly by the existing opentheory infrastructure. By looking at some
>> opentheory tool help texts, I couldn't see the answer to this question. Most
>> of the commands seem to be concerned with package management, which is
>> unrelated. Currently, we do
>> -- mark the last occurrence of any given object, to ensure deletion
>> -- strip material that is not relevant for some "exported" theorem
> 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?
And thanks for the other answers. I will need to play with all this (and
it will take some time as I can only work on it occasionally).
More information about the opentheory-users