**NOTE 1**:
Two proofs in the regression originally failed due to the bug
discussed below, but have been fixed.  You may wish to update your
development copy of ACL2 soon.

**NOTE 2**:
It wouldn't surprise me if there is a Version 6.5 release within a few
days.  If you have any pending commits to the books, you may wish to
get them in soon.

Quoting :doc note-6-5:

  We fixed a soundness bug in how the [tau-system] processed calls of
  if. Thanks to Dmitry Nadezhin for reporting this bug by sending a
  simple example that exploited it to prove nil. To see that example,
  see the comment about ``tau soundess bug'' in the form (defxdoc
  note-6-5 ...) in [community-books] file
  books/system/doc/acl2-doc.lisp.



git-svn-id: http://acl2-devel.googlecode.com/svn/trunk@1348 5d84a466-a78b-0930-a311-59b22171a541