# HG changeset patch
# User haftmann
# Date 1305886194 -7200
# Node ID f115492c7c8ddddb260da6e468fa2c3062ab40dc
# Parent  da1253ff176459dc393a4dc828aa2354657f2225
NEWS

diff -r da1253ff1764 -r f115492c7c8d NEWS
--- a/NEWS	Fri May 20 12:07:17 2011 +0200
+++ b/NEWS	Fri May 20 12:09:54 2011 +0200
@@ -58,15 +58,20 @@
 
 *** HOL ***
 
+* Finite_Set.thy: more coherent development of fold_set locales:
+
+    locale fun_left_comm ~> locale comp_fun_commute
+    locale fun_left_comm_idem ~> locale comp_fun_idem
+    
+Both use point-free characterisation; interpretation proofs may need adjustment.
+INCOMPATIBILITY.
+
 * Code generation:
   - theory Library/Code_Char_ord provides native ordering of characters
     in the target language.
     
 * Declare ext [intro] by default.  Rare INCOMPATIBILITY.
 
-* 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.