Major Section: NOTE-2-8
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.