ACL2-PC::BOOKMARK

(macro) insert matching ``bookends'' comments 
Major Section:  PROOF-CHECKER-COMMANDS


Example:
(bookmark final-goal)

General Form:
(bookmark name &rest instruction-list)
Run the instructions in instruction-list (as though this were a call of do-all; see the documentation for do-all), but first insert a begin bookend with the given name and then, when the instructions have been completed, insert an end bookend with that same name. See the documentation of comm for an explanation of bookends and how they can affect the display of instructions.