diff -r 9ba44b49859b -r 40e60897ee07 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,