Theorem Display Commands

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.