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.
undo some instructions
Major Section: PROOF-CHECKER-COMMANDS
Examples: (undo 7) undoNote: To remove the effect of anGeneral Forms:
(undo n) -- Undo the last n instructions. The argument n should be a positive integer.
undo -- Same as (undo 1).
undo command, use restore. See
the documentation for details.
Note: 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.