Major Section: RELEASE-NOTES
Changed the default distributed books directory for ACL2(r) from
books/ to books/nonstd/. See include-book, in particular the
discussion of ``Distributed Books Directory''.
Added directory books/arithmetic-3/ and its subdirectories to
books/nonstd/. (But a chunk of theorems from
arithmetic-3/extra/ext.lisp are ``commented out'' using
#-:non-standard-analysis because they depend on books/rtl/rel7/, which is
not yet in books/nonstd/; feel free to volunteer to remedy this!)
Incorporated changes from Ruben Gamboa to some (linear and non-linear) arithmetic routines in the theorem prover, to comprehend the reals rather than only the rationals.
Please also see note-3-2 for changes to Version 3.2 of ACL2.
