next up previous contents
Next: Proof Commands Up: Appendix: Reference for Individual Previous: Declaration Commands

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.



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