<div dir="ltr"><div><div><div><div><div><div><div>Hi,<br><br></div>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).<br><br></div>I know there is already this command:<br><br></div>opentheory info --theorems ...<br><br></div>which removes all the proofs, but it still keeps the definitions in.<br><br></div>Can I also remove the definitions?<br><br></div><div>In essence, I want a totally axiomatic presentation of a theory.<br></div><div><br></div>Thanks,<br></div>Ramana</div>