ACL2-PC::SAVE

(macro) save the proof-checker state (state-stack) 
Major Section:  PROOF-CHECKER-COMMANDS


Example:
(save lemma3-attempt)


General Form:
(save &optional name do-it-flg)
Saves the current proof-checker state by ``associating'' it with the given name. Submit (retrieve name) to Lisp to get back to this proof-checker state. If verify was originally supplied with an event name, then the argument can be omitted in favor of that name as the default.

Note that if a save has already been done with the indicated name (or the default event name), then the user will be queried regarding whether to go ahead with the save -- except, if do-it-flg is supplied and not nil, then there will be no query and the save will be effected.

See also the documentation for retrieve and unsave.