Quoting :doc note-6-4:

  Fixed a long-standing soundness bug (found at least as far back as
  Version 1.9!) in the checking done for [congruence] rules. There
  had failed to be a check that the new variable on the right-hand
  side of the conclusion is indeed new. The following example is
  shown in detail as a comment in function
  interpret-term-as-congruence-rule, ACL2 source file defthm.lisp,
  where it is used to prove nil in Version 6.3.

    (implies (e y1 y2)
             (equal (h y2 y1)
                    (h y2 y2)))

Incorporated recent doc fixes from community book
system/doc/acl2-doc.lisp into doc.lisp.


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