insert matching ``bookends'' comments
Major Section: PROOF-CHECKER-COMMANDS
Example: (bookmark final-goal)Run the instructions in
General Form: (bookmark name &rest instruction-list)
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
commfor an explanation of bookends and how they can affect the display of instructions.