NEWS

--- a/NEWS	Sat May 14 00:32:16 2011 +0200
+++ b/NEWS	Sat May 14 18:26:25 2011 +0200
@@ -58,6 +58,9 @@
 
 *** HOL ***
 
+* Finite_Set.thy: locale fun_left_comm uses point-free characterisation;
+interpretation proofs may need adjustment.  INCOMPATIBILITY.
+
 * Nitpick:
   - Added "need" and "total_consts" options.
   - Reintroduced "show_skolems" option by popular demand.