src/HOL/Library/Multiset.thy
changeset 14445 4392cb82018b
parent 13601 fd3e3d6b37b2
child 14691 e1eedc8cad37
     1.1 --- a/src/HOL/Library/Multiset.thy	Mon Mar 08 12:16:57 2004 +0100
     1.2 +++ b/src/HOL/Library/Multiset.thy	Mon Mar 08 12:17:43 2004 +0100
     1.3 @@ -801,7 +801,6 @@
     1.4      apply (rule one_step_implies_mult)
     1.5        apply (simp only: trans_def)
     1.6        apply auto
     1.7 -  apply (blast intro: order_less_trans)
     1.8    done
     1.9  
    1.10  theorem union_upper1: "A <= A + (B::'a::order multiset)"