` `

prettyprint the conclusion, highlighting the current term
Major Section: PROOF-CHECKER-COMMANDS

Example and General Form: p-topFor example, if the conclusion is

`(equal (and x (p y)) (foo z))`

and
the current subterm is `(p y)`

, then `p-top`

will print
`(equal (and x (*** (p y) ***)) (foo z))`

.
Prettyprint the the conclusion, highlighting the current term. The
usual user syntax is used, as with the command `p`

(as opposed to `pp`

).
This is illustrated in the example above, where one would `*not*`

see
`(equal (if x (*** (p y) ***) 'nil) (foo z))`

.

**Remark** (obscure): In some situations, a term of the form `(if x t y)`

occurring inside the current subterm will not print as `(or x y)`

, when
`x`

isn't a call of a boolean primitive. There's nothing incorrect about
this, however.