ACL2-PC::PP

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

Example and General Form:
pp

This is the same as p (see its documentation), except that raw syntax (internal form) is used. So for example, one would see (if x y 'nil) rather than (and x y). Abbreviations are however still inserted, as with p.