July 23, 1997. Version 2.0 is new. It is the first version of ACL2 released from UT. The main motivation for releasing it was to fix a bug in Version 1.9 that, in rare circumstances, caused a pernicious infinite loop.
December 3, 1997. Bishop Brock has written new
documentation for the defstructure book. The book provides
a ``record facility'' similar to Common Lisp's defstruct and
Nqthm's add-shell. Please ignore the documentation that is in
the source file of the book; it was out-of-date when the book was
distributed.