# HG changeset patch
# User Lars Noschinski <noschinl@in.tum.de>
# Date 1288340089 -7200
# Node ID 8792b0b89dcfede790e3c22f4e7d0e8646f4b2bc
# Parent  2107581b404d63e0a978e5e26be8acbf327d90fb# Parent  cd404ecb9107a096ec96cfdb956420e69fb6db18
merged

diff -r 2107581b404d -r 8792b0b89dcf src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Fri Oct 29 08:44:49 2010 +0200
+++ b/src/HOL/Library/Multiset.thy	Fri Oct 29 10:14:49 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)"