NOTE-2-6-RULES

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