changeset 49822 | 0cfc1651be25 |
parent 49770 | cf6a78acf445 |
child 49836 | c13b39542972 |
--- a/NEWS Thu Oct 11 00:13:21 2012 +0200 +++ b/NEWS Thu Oct 11 11:56:42 2012 +0200 @@ -62,6 +62,16 @@ *** HOL *** +* Theory "Library/Multiset": + + - Renamed constants + fold_mset ~> Multiset.fold -- for coherence with other fold combinators + + - Renamed facts + fold_mset_commute ~> fold_mset_comm -- for coherence with fold_comm + +INCOMPATIBILITY. + * Theorem UN_o generalized to SUP_comp. INCOMPATIBILITY. * Class "comm_monoid_diff" formalises properties of bounded