ACL2-PC::RETRIEVE

(macro) re-enter the proof-checker 
Major Section:  PROOF-CHECKER-COMMANDS


Examples:
(retrieve associativity-of-permutationp)
retrieve


General Form:
(retrieve &optional name)
Must be used from outside the interactive proof-checker loop. If name is supplied and not nil, this causes re-entry to the interactive proof-checker loop in the state at which save was last executed for the indicated name. (See documentation for save.) If name is nil or is not supplied, then the user is queried regarding which proof-checker state to re-enter. The query is omitted, however, if there only one proof-checker state is present that was saved with save, in which case that is the one that is used. See also unsave.