NEWS
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.