Major Section: NOTE-2-8
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
defevaluator event has been modified so that in the body of the
evaluator function, to add a new case
(ATOM X) (returning
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.
imagpart-+ have been added in order
to simplify the
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.