ACL2-PC::UNDO

(meta) 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.