ACL2-pc::unsave
(macro)
remove a proof-builder state
Example:
(unsave assoc-of-append)
General Form:
(unsave &optional name)
Eliminates the association of an interactive proof-builder state with
name, if name is supplied and not nil. The name may be
nil or not supplied, in which case it defaults to the event name supplied
with the original call to verify (if there is one — otherwise, the
instruction ``fails'' and there is no change). The ACL2 function unsave
may also be executed outside the interactive loop, with the same syntax.
Also see ACL2-pc::save and ACL2-pc::retrieve.
