Quoting :doc note-6-4:

  The class of [congruence] rules has been broadened considerably, so
  that one can restrict to patterns. For example, a congruence rule
  can now state that an equivalence is maintained for the term
  (mv-nth 1 (f (cons u v) y 'a)) when rewriting y. See
  [patterned-congruence]. Thanks to Sol Swords for requesting this
  feature.


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