ACL2-PC::RESTORE

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

Remark: 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).