next up previous contents
Next: Reaxiomatization and Redefinition Up: The Theory Environment Previous: Special Declarations


Entry of theorems into the theorem list is usually via the proof and definition commands. Axioms can be entered using the axiom command, which takes name, left side, and right side of the axiom as parameters, or using the interaxiom command, which interprets the selected subterm of the right side of the current equation as an equation (so it needs to be one!) and enters it as an axiom with a name supplied as a parameter.

One views a single theorem using the thmdisplay command. One can view all theorems using showalltheorems or scanthms. One can view the module associated with a theorem using moddisplay, or view all modules using showallmodules. One can view a theorem matching a given equation using showmatchthm. One can view a list of theorems applicable to the selected subterm (excluding theorems applicable to every term) using showrelevantthms. One can view all saved environments using showsavedenvs. One can view all axioms and definitions using showallaxioms.

Randall Holmes
Fri Sep 5 16:28:58 MDT 1997