` `

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`

!).