Rule
A thm-like version of defrule.
The rule macro is a thin wrapper around defrule. It
supports all of the same syntax extensions like top-level :enable and
:expand ACL2::hints. However, like thm, rule does not
take a rule name and does not result in the introduction of a rule
afterward.
Examples:
(rule (implies x x)) ;; will work
(rule (equal (append x y) ;; will fail
(append y x))
:enable append
:expand (append y x))
(rule (equal (consp x) ;; will work
(if (atom x) nil t))
:do-not '(generalize fertilize))
The rule command is implemented with a simple make-event, and
its calls are valid embedded events. However, on
success a rule merely expands into (value-triple :success). No
record of the rule's existence is found in the world, so there is no way to use
the rule once it has been proven, etc.
