[opentheory-users] Scalable LCF-style proof translation

[Alexander Krauss]

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

Alex