# HG changeset patch
# User Lars Noschinski <noschinl@in.tum.de>
# Date 1285142199 -7200
# Node ID cd404ecb9107a096ec96cfdb956420e69fb6db18
# Parent  922634ecdda4447346f296634c548704868864e8
Remove unnecessary premise of mult1_union

diff -r 922634ecdda4 -r cd404ecb9107 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Sep 21 14:42:29 2010 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed Sep 22 09:56:39 2010 +0200
@@ -1279,7 +1279,7 @@
 subsubsection {* Monotonicity of multiset union *}
 
 lemma mult1_union:
-  "(B, D) \<in> mult1 r ==> trans r ==> (C + B, C + D) \<in> mult1 r"
+  "(B, D) \<in> mult1 r ==> (C + B, C + D) \<in> mult1 r"
 apply (unfold mult1_def)
 apply auto
 apply (rule_tac x = a in exI)
@@ -1290,8 +1290,8 @@
 lemma union_less_mono2: "B \<subset># D ==> C + B \<subset># C + (D::'a::order multiset)"
 apply (unfold less_multiset_def mult_def)
 apply (erule trancl_induct)
- apply (blast intro: mult1_union transI order_less_trans r_into_trancl)
-apply (blast intro: mult1_union transI order_less_trans r_into_trancl trancl_trans)
+ apply (blast intro: mult1_union)
+apply (blast intro: mult1_union trancl_trans)
 done
 
 lemma union_less_mono1: "B \<subset># D ==> B + C \<subset># D + (C::'a::order multiset)"