Two soundness bugs have been reported: a bug in functional instantiation found
by Francisco J. Martin-Mateos, and a bug in :bdd hints found by Rob Sumners.
Please see our patch page for information on how
to get a corrected copy of ACL2.
The nonstandard analysis books have been updated, as Ruben Gamboa has
graciously eliminated some skip-proofs events. The gzipped tar file can be
obtained from the usual place (click here).