The display command displays information of the requested
<information-type> about all facts and conjectures with names matching
<names>. If <information-type> is omitted, it is assumed to be facts.
Displays all unproved conjectures [with the specified names].
display facts [ <names> ]
Displays all facts in the current proof context [with the specified names].
Indicates immune facts by an (I) following
their names, ancestor-immune statements by an (i), and
passive facts by a (P).
display names
Displays all name-prefixes introduced in the current proof context.
display ordering-constraints [ <names> ]
Displays the registry for all operators [in the
named facts] in the current proof context, unless the value of the
ordering-method setting is polynomial, in which case it displays
the polynomial interpretations of these
operators.
display proof-status
Displays the status of the current conjecture and all other conjectures for
which it is a subgoal (of a subgoal ...).
display symbols [ <names> ]
Displays all sorts, operators, and variables [in the named facts] in the
current proof context. The command display symbols displays all symbols
in the current proof context, whereas display symbols * only displays
those that occur in some fact.