restore command always ``succeeds''; it returns
(mv nil t state).
remove the effect of an UNDO command
Major Section: PROOF-CHECKER-COMMANDS
Example and General Form: restore
Restore removes the effect of an undo command. This always works as
expected if restore is invoked immediately after undo, without
intervening instructions. However, other commands may also interact
with restore, notably ``sequencing'' commands such as do-all,
do-strict, protect, and more generally, sequence.
Note: Another way to control the saving of proof-checker state is
with the save command; see the documentation for save.
The restore command always ``succeeds''; it returns
(mv nil t state).