ACL2-pc::restore
(meta)
remove the effect of an UNDO command
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-builder state is
with the save command; see ACL2-pc::save.
The restore command always ``succeeds''; it returns (mv nil t
state).
