--- a/NEWS Tue Nov 30 20:02:01 2010 -0800
+++ b/NEWS Wed Dec 01 11:45:37 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.