NOTE-2-7(R)

ACL2 Version 2.7(r) (November, 2002) Notes
Major Section:  RELEASE-NOTES

In source file axioms.lisp, in order for proofs to succeed, (make proofs), the definitions of acl2-count and explode-atom have been modified slightly, and lemma standard-numberp-one [modified after Version_3.4 to become standardp-one] has been given :rule-classes nil.

All skip-proofs forms have been eliminated from the nonstd books, thanks to Ruben Gamboa.

The directory books/sqrt/, which was intended for ACL2(r), has been moved to books/nonstd/sqrt/ and added as appropriate to books/nonstd/Makefile.

Please see note-2-7 for changes to Version_2.7 of ACL2.