changeset 69316 | 248696d0a05f |
parent 69282 | 94fa3376ba33 |
child 69343 | 395c4fb15ea2 |
--- a/NEWS Sun Nov 18 18:07:51 2018 +0000 +++ b/NEWS Mon Nov 19 13:40:04 2018 +0100 @@ -54,6 +54,8 @@ * Theory "HOL-Library.Multiset": the <Union># operator now has the same precedence as any other prefix function symbol. +* Retired lemma card_Union_image; use the simpler card_UN_disjoint instead. + * Facts sum_mset.commute and prod_mset.commute renamed to sum_mset.swap and prod_mset.swap, similarly to sum.swap and prod.swap. INCOMPATIBILITY.