# HG changeset patch
# User nipkow
# Date 1519044976 -3600
# Node ID 59feb83c6ab958b18e2f0f0d584501c29deb7c17
# Parent  8f4810b9d9d1afffa7a532249f1b0ef34fe7f5dd
added lemma

diff -r 8f4810b9d9d1 -r 59feb83c6ab9 src/HOL/Library/Multiset.thy
--- 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