Major Section: NOTE-2-7
The defcong macro has been slightly changed. The difference is that
the variable generated with suffix -EQUIV will now be in the same package
as the name of the variable from which it is generated, rather than always
belonging to the ACL2 package. Thanks to Hanbing Liu for suggesting this
change. (Note that a couple of books have been modified to accommodate this
change, e.g., books/finite-set-theory/set-theory.)
In Version_2.6, a change was made for rules of class :rewrite whose
conclusion is a term of the form (EQV lhs rhs), where EQV is =,
eq, or eql: the rule was stored as though EQV were
equal. (See note-2-6-rules.) This change has been extended to rules
of class :definition.