ACL2-pc::save
(macro)
save the proof-builder state (state-stack)
Example:
(save lemma3-attempt)
General Form:
(save &optional name do-it-flg)
Saves the current state of the interactive proof-builder by ``associating''
it with the given name, which must be a symbol. Submit (retrieve name)
to Lisp to get back to this proof-builder state. If verify was
originally supplied with an event name, then the argument can be omitted in
favor of that name as the default.
Remark 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.
Also see ACL2-pc::retrieve and ACL2-pc::unsave.
