# HG changeset patch
# User haftmann
# Date 1291200337 -3600
# Node ID 5a2ae8cc9d0e619c68a300a4e496cdfe19740758
# Parent  fc750e794458daa7e4d5fdcdbb5514afc3aeb9d9
NEWS

diff -r fc750e794458 -r 5a2ae8cc9d0e NEWS
--- 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.