src/HOL/Library/Multiset.thy
changeset 40249 cd404ecb9107
parent 39533 91a0ff0ff237
child 40250 8792b0b89dcf
     1.1 --- a/src/HOL/Library/Multiset.thy	Tue Sep 21 14:42:29 2010 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Wed Sep 22 09:56:39 2010 +0200
     1.3 @@ -1279,7 +1279,7 @@
     1.4  subsubsection {* Monotonicity of multiset union *}
     1.5  
     1.6  lemma mult1_union:
     1.7 -  "(B, D) \<in> mult1 r ==> trans r ==> (C + B, C + D) \<in> mult1 r"
     1.8 +  "(B, D) \<in> mult1 r ==> (C + B, C + D) \<in> mult1 r"
     1.9  apply (unfold mult1_def)
    1.10  apply auto
    1.11  apply (rule_tac x = a in exI)
    1.12 @@ -1290,8 +1290,8 @@
    1.13  lemma union_less_mono2: "B \<subset># D ==> C + B \<subset># C + (D::'a::order multiset)"
    1.14  apply (unfold less_multiset_def mult_def)
    1.15  apply (erule trancl_induct)
    1.16 - apply (blast intro: mult1_union transI order_less_trans r_into_trancl)
    1.17 -apply (blast intro: mult1_union transI order_less_trans r_into_trancl trancl_trans)
    1.18 + apply (blast intro: mult1_union)
    1.19 +apply (blast intro: mult1_union trancl_trans)
    1.20  done
    1.21  
    1.22  lemma union_less_mono1: "B \<subset># D ==> B + C \<subset># D + (C::'a::order multiset)"