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)
Verifyis the function used for entering the proof-checker's interactive loop.