term!).
prettyprint the current term
Major Section: PROOF-CHECKER-COMMANDS
Example and General Form: p
Prettyprint the current term. The usual user syntax is used, so
that for example one would see (and x y) rather than (if x y 'nil).
(See also pp.) Also, abbreviations are inserted where appropriate;
see add-abbreviation.
The ``current term'' is the entire conclusion unless dive commands
have been given, in which case it may be a subterm of the
conclusion.
If all goals have been proved, a message saying so will be printed
(as there will be no current term!).