--- 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.