ACL2-PC::PRINT-ALL-GOALS

(macro) print all the (as yet unproved) goals
Major Section:  PROOF-CHECKER-COMMANDS

Example and General Form: print-all-goals

Prints all the goals that remain to be proved, in a pleasant format. See also the proof-checker command print-all-concs.