| changeset 67656 | 59feb83c6ab9 |
| parent 67398 | 5eb932e604a2 |
| child 68249 | 949d93804740 |
--- a/src/HOL/Library/Multiset.thy Sun Feb 18 20:08:21 2018 +0100 +++ b/src/HOL/Library/Multiset.thy Mon Feb 19 13:56:16 2018 +0100 @@ -2407,6 +2407,9 @@ lemma Union_mset_empty_conv[simp]: "\<Union># M = {#} \<longleftrightarrow> (\<forall>i\<in>#M. i = {#})" by (induction M) auto +lemma Union_image_single_mset[simp]: "\<Union># (image_mset (\<lambda>x. {#x#}) m) = m" +by(induction m) auto + context comm_monoid_mult begin