# HG changeset patch
# User nipkow
# Date 1273670723 -7200
# Node ID b78d3c87fc889c5012b191a1c2e083272fe49f83
# Parent  59ed5370014570ec1be711195cc3803ae81dc211# Parent  6c28c702ed22039e1fc8afc6b2abb6ac9361cfda
merged

diff -r 59ed53700145 -r b78d3c87fc88 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed May 12 13:34:24 2010 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed May 12 15:25:23 2010 +0200
@@ -330,24 +330,8 @@
   by (simp add: multiset_eq_conv_count_eq mset_le_def)
 
 lemma mset_le_multiset_union_diff_commute:
-  assumes "B \<le> A"
-  shows "(A::'a multiset) - B + C = A + C - B"
-proof -
-  from mset_le_exists_conv [of "B" "A"] assms have "\<exists>D. A = B + D" ..
-  from this obtain D where "A = B + D" ..
-  then show ?thesis
-    apply simp
-    apply (subst add_commute)
-    apply (subst multiset_diff_union_assoc)
-    apply simp
-    apply (simp add: diff_cancel)
-    apply (subst add_assoc)
-    apply (subst add_commute [of "B" _])
-    apply (subst multiset_diff_union_assoc)
-    apply simp
-    apply (simp add: diff_cancel)
-    done
-qed
+  "B \<le> A \<Longrightarrow> (A::'a multiset) - B + C = A + C - B"
+by (simp add: multiset_eq_conv_count_eq mset_le_def)
 
 lemma mset_lessD: "A < B \<Longrightarrow> x \<in># A \<Longrightarrow> x \<in># B"
 apply (clarsimp simp: mset_le_def mset_less_def)