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.