--- a/NEWS Wed Dec 01 15:35:40 2010 +0100
+++ b/NEWS Wed Dec 01 15:38:05 2010 +0100
@@ -92,8 +92,8 @@
*** HOL ***
-* Abandoned locale equiv for equivalence relations. INCOMPATIBILITY: use
-equivI rather than equiv_intro.
+* Abandoned locales equiv, congruent and congruent2 for equivalence relations.
+INCOMPATIBILITY: use equivI rather than equiv_intro (same for congruent(2)).
* Code generator: globbing constant expressions "*" and "Theory.*" have been
replaced by the more idiomatic "_" and "Theory._". INCOMPATIBILITY.