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.