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.
