Major Section: PROOF-CHECKER

Examples: (retrieve associativity-of-permutationp) retrieveSee acl2-pc::retrieve, or useGeneral Form: (retrieve &optional name)

`(help retrieve)`

inside the
interactive proof-checker loop. Also see unsave.
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.
Major Section: PROOF-CHECKER

Example: (unsave assoc-of-append)Eliminates the association of a proof-checker state withGeneral Form: (unsave name)

`name`

.
See unsave or see acl2-pc::unsave.
Also see acl2-pc::save and see retrieve.

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.