Major Section: RELEASE-NOTES
Important changes:
We corrected a soundness bug in Version 2.3 related to the handling of
immediate-force-modep. The bad behavior was noticed by Robert
Krug. Thanks!
We corrected a bug that permitted verify-guards to accept a function
even though a subfunction had not yet had its guards verified. Thanks to
John Cowles for noticing this.
User defined single-threaded objects are now supported. See stobj.
Less important notes:
We corrected a bug that prevented the intended expansion of some recursive function calls.
We changed the handling of the primitive function ILLEGAL, which
is logically defined to be nil but which is programmed to signal an
error, so that when it is evaluated as part of a proof, it does not signal
an error. The old handling of the function prevented some guard proofs
involving THE or LETs with internal declarations.
We corrected a bug that permitted some LOCAL DEFAXIOM events to slip
into certified books.
We corrected a bug that prevented the correct undoing of certain DEFPKG
forms.
Changes were made to support CMU Lisp. Pete Manolios helped with these changes.
Changes were made to make the make files more compatible with Allegro Common Lisp. Jun Sawada, who has been a great help with keeping ACL2 up and running at UT on various platforms, was especially helpful. Thanks Jun.