RETRIEVE

re-enter a (specified) proof-checker state 
Major Section:  PROOF-CHECKER


Examples:
(retrieve associativity-of-permutationp)
retrieve


General Form:
(retrieve &optional name)
See acl2-pc::retrieve, or use (help retrieve) inside the interactive proof-checker loop. Also see unsave.












































































TOGGLE-PC-MACRO

change an ordinary macro command to an atomic macro, or vice-versa 
Major Section:  PROOF-CHECKER


Example:
(toggle-pc-macro pro)
Change pro from an atomic macro command to an ordinary one (or vice-versa, if pro happens to be an ordinary macro command) 

General Form:
(toggle-pc-macro name &optional new-tp)
If name is an atomic macro command then this turns it into an ordinary one, and vice-versa. However, if new-tp is supplied and not nil, then it should be the new type, or else there is no change.












































































UNSAVE

remove a proof-checker state 
Major Section:  PROOF-CHECKER


Example:
(unsave assoc-of-append)


General Form:
(unsave name)
Eliminates the association of a proof-checker state with name. See unsave or see acl2-pc::unsave.

Also see acl2-pc::save and see retrieve.












































































VERIFY

enter the interactive proof checker 
Major Section:  PROOF-CHECKER

For proof-checker command summaries, see proof-checker. 

Examples:
(VERIFY (implies (and (true-listp x) (true-listp y))
                      (equal (append (append x y) z)
                             (append x (append y z)))))
   -- Attempt to prove the given term interactively.


(VERIFY (p x)
        :event-name p-always-holds
        :rule-classes (:rewrite :generalize)
        :instructions ((rewrite p-always-holds-lemma)
                       change-goal))
   -- Attempt to prove (p x), where the intention is to call the
      resulting DEFTHM event by the name p-always-holds, with
      rule-classes as indicated.  The two indicated instructions
      will be run immediately to start the proof.


(VERIFY)
   -- Re-enter the proof-checker in the state at which is was last
      left.


General Form:
(VERIFY &OPTIONAL raw-term
        &KEY
        event-name
        rule-classes
        instructions)
Verify is the function used for entering the proof-checker's interactive loop.