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.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.
See also the documentation for retrieve
and unsave
.