# HG changeset patch # User Lars Noschinski # 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) \ mult1 r ==> trans r ==> (C + B, C + D) \ mult1 r" + "(B, D) \ mult1 r ==> (C + B, C + D) \ mult1 r" apply (unfold mult1_def) apply auto apply (rule_tac x = a in exI) @@ -1290,8 +1290,8 @@ lemma union_less_mono2: "B \# D ==> C + B \# 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 \# D ==> B + C \# D + (C::'a::order multiset)"