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