ACL2-PC::P-TOP

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

Example and General Form:
p-top
For 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.