ACL2-PC::UNSAVE

(macro) remove a proof-checker state 
Major Section:  PROOF-CHECKER-COMMANDS


Example:
(unsave assoc-of-append)


General Form:
(unsave &optional name)
Eliminates the association of a proof-checker 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.

See also documentation for save and retrieve.