Next: Proof Commands
Up: Appendix: Reference for Individual
Previous: Declaration Commands
- ``thmdisplay thm'' causes theorem ``thm'' to be
displayed. (walk command ``D''). Displays comments. Displays
names but not contents of module components (hidden theorems).
- 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''
- moddisplay, showallmodules
- As thmdisplay, showalltheorems,
except that module contents are displayed.
- Displays the theorem (if any) bound to a constant
- Displays all programs.
- ``seedef defined'' displays the defining theorem of the
constant or operator ``defined''.
- Displays all definitions.
- 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.
- Displays all axioms and definitions.
Fri Sep 5 16:28:58 MDT 1997