--- a/NEWS Wed Apr 18 20:45:48 2012 +0200
+++ b/NEWS Wed Apr 18 20:47:21 2012 +0200
@@ -302,8 +302,7 @@
* Finite_Set.fold now qualified. INCOMPATIBILITY.
-* Consolidated various theorem names relating to Finite_Set.fold
-combinator:
+* Consolidated theorem names concerning fold combinators:
inf_INFI_fold_inf ~> inf_INF_fold_inf
sup_SUPR_fold_sup ~> sup_SUP_fold_sup
@@ -311,11 +310,6 @@
SUPR_fold_sup ~> SUP_fold_sup
union_set ~> union_set_fold
minus_set ~> minus_set_fold
-
-INCOMPATIBILITY.
-
-* Consolidated theorem names concerning fold combinators:
-
INFI_set_fold ~> INF_set_fold
SUPR_set_fold ~> SUP_set_fold
INF_code ~> INF_set_foldr
@@ -325,6 +319,9 @@
foldl_fold ~> foldl_conv_fold
foldr_foldr ~> foldr_conv_foldl
foldl_foldr ~> foldl_conv_foldr
+ fold_set_remdups ~> fold_set_fold_remdups
+ fold_set ~> fold_set_fold
+ fold1_set ~> fold1_set_fold
INCOMPATIBILITY.
@@ -347,16 +344,6 @@
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.