1.1 --- a/NEWS	Fri May 20 12:07:17 2011 +0200
     1.2 +++ b/NEWS	Fri May 20 12:09:54 2011 +0200
     1.3 @@ -58,15 +58,20 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Finite_Set.thy: more coherent development of fold_set locales:
     1.8 +
     1.9 +    locale fun_left_comm ~> locale comp_fun_commute
    1.10 +    locale fun_left_comm_idem ~> locale comp_fun_idem
    1.11 +    
    1.12 +Both use point-free characterisation; interpretation proofs may need adjustment.
    1.13 +INCOMPATIBILITY.
    1.14 +
    1.15  * Code generation:
    1.16    - theory Library/Code_Char_ord provides native ordering of characters
    1.17      in the target language.
    1.18      
    1.19  * Declare ext [intro] by default.  Rare INCOMPATIBILITY.
    1.20  
    1.21 -* Finite_Set.thy: locale fun_left_comm uses point-free characterisation;
    1.22 -interpretation proofs may need adjustment.  INCOMPATIBILITY.
    1.23 -
    1.24  * Nitpick:
    1.25    - Added "need" and "total_consts" options.
    1.26    - Reintroduced "show_skolems" option by popular demand.