Major Section: RELEASE-NOTES
We corrected a soundness bug in Version 2.3 related to the handling of
immediate-force-modep. The bad behavior was noticed by Robert
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
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
LETs with internal declarations.
We corrected a bug that permitted some
DEFAXIOM events to slip
into certified books.
We corrected a bug that prevented the correct undoing of certain
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.