ACL2-pc::retrieve
(macro)
re-enter the proof-builder
Examples:
(retrieve associativity-of-permutationp)
retrieve
General Form:
(retrieve &optional name)
Must be used from outside the interactive proof-builder loop. If name
(which must be a symbol) is supplied and not nil, this causes re-entry to
the interactive proof-builder loop in the state at which save was last
executed for the indicated name. (See ACL2-pc::save.) If name is
nil or is not supplied, then the user is queried regarding which
proof-builder state to re-enter. The query is omitted, however, if there only
one proof-builder state is present that was saved with save, in which
case that is the one that is used. Also see ACL2-pc::unsave.
