ACL2-pc::bookmark
(macro)
insert matching ``bookends'' comments
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 ACL2-pc::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 ACL2-pc::comm for an
explanation of bookends and how they can affect the display of
instructions.
