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