Note-2-6-rules
ACL2 Version 2.6 Notes on Changes in Rules and Constants
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.
