undo some instructions
(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 ACL2-pc::restore.
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.