--- a/NEWS Wed Apr 18 20:40:52 2012 +0200
+++ b/NEWS Wed Apr 18 20:45:48 2012 +0200
@@ -300,6 +300,8 @@
* Removed redundant theorems nat_mult_2 and nat_mult_2_right; use
generic mult_2 and mult_2_right instead. INCOMPATIBILITY.
+* Finite_Set.fold now qualified. INCOMPATIBILITY.
+
* Consolidated various theorem names relating to Finite_Set.fold
combinator:
@@ -345,6 +347,16 @@
lemmas over fold rather than foldr, or make use of lemmas
fold_conv_foldr and fold_rev.
+* Renamed some facts on canonical fold on lists, in order to avoid
+problems with interpretation involving corresponding facts on foldl
+with the same base names:
+
+ fold_set_remdups ~> fold_set_fold_remdups
+ fold_set ~> fold_set_fold
+ fold1_set ~> fold1_set_fold
+
+INCOMPATIBILITY.
+
* Congruence rules Option.map_cong and Option.bind_cong for recursion
through option types.
@@ -357,18 +369,6 @@
* Discontinued configuration option "syntax_positions": atomic terms
in parse trees are always annotated by position constraints.
-* Finite_Set.fold now qualified. INCOMPATIBILITY.
-
-* Renamed some facts on canonical fold on lists, in order to avoid
-problems with interpretation involving corresponding facts on foldl
-with the same base names:
-
- fold_set_remdups ~> fold_set_fold_remdups
- fold_set ~> fold_set_fold
- fold1_set ~> fold1_set_fold
-
-INCOMPATIBILITY.
-
* New theory HOL/Library/DAList provides an abstract type for
association lists with distinct keys.