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

Fri Sep 5 16:28:58 MDT 1997