undo some instructions
Major Section: PROOF-CHECKER-COMMANDS
Examples:
(undo 7)
undo
General Forms:
(undo n) -- Undo the last n instructions. The argument n should be
a positive integer.
undo -- Same as (undo 1).
Remark: To remove the effect of an undo command, use restore.
See the documentation for details.Remark: If the argument n is greater than the total number of
interactive instructions in the current session, then (undo n) will
simply take you back to the start of the session.
The undo meta command always ``succeeds''; it returns
(mv nil t state) unless its optional argument is supplied and of
the wrong type (i.e. not a positive integer) or there are no
instructions to undo.
