# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1519058825 0
# Node ID 67909bfc392340d9311467e00288130d718f325f
# Parent  c8caefb20564c67d45a8670c9f1398ca64af2a1e# Parent  59feb83c6ab958b18e2f0f0d584501c29deb7c17
Merge

diff -r c8caefb20564 -r 67909bfc3923 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Feb 19 16:44:45 2018 +0000
+++ b/src/HOL/Library/Multiset.thy	Mon Feb 19 16:47:05 2018 +0000
@@ -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