**thmdisplay**- ``thmdisplay thm'' causes theorem ``thm'' to be
displayed. (walk command ``D''). Displays comments. Displays
names but not contents of module components (hidden theorems).
**showalltheorems**- Causes a theorem to be displayed with each
keystroke (most recently proved first). Any key other than Enter
breaks out. (walk command ``T'' has a similar function; use ``l''
and ``r'' to scan through the theorem list after issuing the ``T''
command)
**moddisplay, showallmodules**- As thmdisplay, showalltheorems,
except that module contents are displayed.
**seeprogram**- Displays the theorem (if any) bound to a constant
or operator.
**seeallprograms**- Displays all programs.
**seedef**- ``seedef defined'' displays the defining theorem of the
constant or operator ``defined''.
**seealldefs**- Displays all definitions.
**showrelevantthms**- Displays theorems applicable to the current
subterm. Will not display theorems which apply to
*all*terms. Hitting any key other than Enter will break out. **showallaxioms**- Displays all axioms and definitions.

Fri Sep 5 16:28:58 MDT 1997