Major Section: NOTE-2-6
The following symbols have been added to the list constant
*common-lisp-specials-and-constants*: REPLACE, FILL, CHARACTER,
=, BREAK, and PRIN1. This was done in support of ports to
Allegro 6.0 and Windows platforms (see note-2-6-new-functionality).
The list of symbols in *acl2-exports* has been modified, for
example to include show-accumulated-persistence and the legal
arguments to set-inhibit-output-lst.
Functions zp and zip are now handled slightly differently. They are
are now disabled, but each comes with a :rewrite rule that allows
their expansion on non-variable terms, and also with a
:compound-recognizer rule that avoids the need for opening up these
functions when applied to variables. The resulting behavior should
be very similar to the behavior of previous versions, except that
case splits will be avoided when these functions are applied to
variables.
Function standard-string-alistp replaces function
string-alistp. For further discussion, see note-2-6-guards.
Rules of class :rewrite whose conclusion is a term of the form
(equal lhs rhs) have always been stored in the expected way: lhs
rewrites to rhs. This way of storing :rewrite rules has been
extended to allow =, eq, or eql in place of equal.
Rewrite rule nth-update-nth, in source file axioms.lisp, has been
strengthened.
A new rewrite rule equal-constant-+ has been added to the book
arithmetic/equalities. This should generally be a beneficial
change, but existing proofs involving the arithmetic books could
conceivably be affected.
Function symbol-package-name and constant *main-lisp-package-name*
have undergone small changes. This change should rarely be noticed
by users and is discussed elsewhere; see note-2-6-system.
We mention here that proofs involving stobjs may need to be modified
because of changes in auxiliary functions generated by defstobj.
(These changes were made in support of a new resizing capability,
mentioned elsewhere in these release notes;
see note-2-6-new-functionality.
In the distributed book directory books/arithmetic/, the book
rationals-with-axioms-proved.lisp has been renamed rationals.lisp.
(ACL2(r) only) Rewrite rules realp-+, realp-*, realp-unary--, and
realp-unary-/ have been added in analogy to existing rules
rationalp-+, rationalp-*, rationalp-unary--, and rationalp-unary-/.
Thanks to Jun Sawada for suggesting this change.
The definition of aref1 has been modified slightly. Previously, if
*my-a* were an array then (aref1 'some-name *my-a* :header) would
evaluate to the cdr of the header of *my-a* rather than to its
default. See arrays.
Changes have been made in the ihs books, based on suggestions from
Jun Sawada, that support its use with ACL2(r) (see real). The
primary change is to replace calls of rationalp with calls of
real/rationalp, which should have no effect on users of standard
ACL2.