NEWS: unavoidable fact renames
authorhaftmann
Mon, 26 Dec 2011 22:17:10 +0100
changeset 45988 40e60897ee07
parent 45987 9ba44b49859b
child 45989 b39256df5f8a
NEWS: unavoidable fact renames
NEWS
--- a/NEWS	Mon Dec 26 18:32:43 2011 +0100
+++ b/NEWS	Mon Dec 26 22:17:10 2011 +0100
@@ -53,6 +53,15 @@
 
 *** HOL ***
 
+* 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.
+
 * 'set' is now a proper type constructor.  Definitions mem_def and Collect_def
 have disappeared.  INCOMPATIBILITY, rephrase sets S used as predicates by
 `%x. x : S` and predicates P used as sets by `{x. P x}`.  For typical proofs,