ACL2 Version 2.4 (August, 1999) 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 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
We corrected a bug that permitted some
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.