[opentheory-users] removing definitions from theories

Ramana Kumar ramana at member.fsf.org
Fri Jan 29 08:36:42 UTC 2016


Hi,

Is it possible to take a theory that makes definitions of types/constants,
and then re-present the same theory _without_ making the definitions
(instead taking them as ungrounded constants, and the definitional theorems
as axioms).

I know there is already this command:

opentheory info --theorems ...

which removes all the proofs, but it still keeps the definitions in.

Can I also remove the definitions?

In essence, I want a totally axiomatic presentation of a theory.

Thanks,
Ramana
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20160129/098edc34/attachment.html>


More information about the opentheory-users mailing list