ACL2-PC::PRINT-MAIN

(macro) print the original goal
Major Section:  PROOF-CHECKER-COMMANDS

Example and General Form:
print-main

Print the goal as originally entered.