DEFAXIOM

add an axiom
Major Section:  EVENTS

WARNING: We strongly recommend that you not add axioms. If at all possible you should use defun or mutual-recursion to define new concepts recursively or use encapsulate to constrain them constructively. If your goal is to defer a proof by using a top-down style, consider using skip-proofs; see the discussion on ``Top-Down Proof'' in Section B.1.2 of ``Computer-Aided Reasoning: An Approach.'' Adding new axioms frequently renders the logic inconsistent.

Example:
(defaxiom sbar (equal t nil)
          :rule-classes nil
          :doc ":Doc-Section ...")

General Form:
(defaxiom name term
         :rule-classes rule-classes
         :doc          doc-string)
where name is a new symbolic name (see name), term is a term intended to be a new axiom, and rule-classes and doc-string are as described in the corresponding documentation topics . The two keyword arguments are optional. If :rule-classes is not supplied, the list (:rewrite) is used; if you wish the axiom to generate no rules, specify :rule-classes nil.