Note-2-8-rules
ACL2 Version 2.8 Notes on Changes in Rules, Definitions, and Constants
The theory minimal-theory has been changed by adding
the definition rune for mv-nth to the theory. A
corresponding change has been made to the theory warning mechanism, which was
failing to warn if the definition of mv-nth is disabled, even though
calls of mv-nth can be expanded by special-purpose code in the rewriter.
Thanks to Serita Van Groningen for pointing out this problem with the theory
warning mechanism.
The defevaluator event has been modified so that in the body of the
evaluator function, to add a new case (ATOM X) (returning nil) has
been inserted immediately after the case (EQ (CAR X) 'QUOTE). This is a
no-op semantically but may speed up proofs. Thanks to Warren Hunt for
suggesting this change.
A new form of :compound-recognizer rule is now allowed:
(if (fn x) concl1 concl2)
This is equivalent to an existing form:
(and (implies (fn x) concl1)
(implies (not (fn x)) concl2))
Thanks to Josh Purinton for bringing this to our attention.
Rewrite rules realpart-+ and imagpart-+ have been added in order
to simplify the realpart and imagpart (respectively) of a sum.
They follow from a theorem add-def-complex that equates a sum with the
complex number formed by adding real and imaginary parts. All three of these
theorems may be found in source file axioms.lisp. Thanks to Eric Smith
for raising a question leading to these additions, as well as to Joe Hendrix
and Vernon Austel for helpful suggestions.
