[opentheory-users] extending the standard library

[Joe Leslie-Hurd]

>> What would be useful is infrastructure for manipulating theories, e.g.,
>> alpha-renaming theorems, or splitting their conjuncts, or whatever stylistic
>> tweaks you want, or removing exported theorems... all after they have been
>> recorded, at the OpenTheory stage, and without requiring lots of long
>> replaying of articles. I don't suppose you have anything like this?
>
> Sorry, I don't. The opentheory tool is a command-line tool now and for
> the foreseeable future, and the operations you describe seem more
> easily handled by a read-eval-print-loop like the one inside a theorem
> prover.

Just one thing that occurred to me after posting this: I could see
incorporating such operations into the existing OpenTheory
infrastructure as part of the repository web interface. It seems to me
that a web browser would be a good interface to perform these kind of
operations on theories, but of course it would still be a significant
engineering effort.

Cheers,

Joe