Mercurialisabelle / diff
summary | shortlog | changelog | graph | tags | branches | files | changeset | file | revisions | annotate | diff | raw
src/HOL/Library/BigO.thy
changeset 45270 d5b5c9259afd
parent 42285 8d91a85b6d91
child 47108 2a1953f0d20d 
     1.1 --- a/src/HOL/Library/BigO.thy	Tue Oct 25 16:37:11 2011 +0200
     1.2 +++ b/src/HOL/Library/BigO.thy	Thu Oct 27 07:46:57 2011 +0200
     1.3 @@ -129,9 +129,6 @@
     1.4    apply (erule order_trans)
     1.5    apply (simp add: ring_distribs)
     1.6    apply (rule mult_left_mono)
     1.7 -  apply assumption
     1.8 -  apply (simp add: order_less_le)
     1.9 -  apply (rule mult_left_mono)
    1.10    apply (simp add: abs_triangle_ineq)
    1.11    apply (simp add: order_less_le)
    1.12    apply (rule mult_nonneg_nonneg)
    1.13 @@ -150,9 +147,6 @@
    1.14    apply (erule order_trans)
    1.15    apply (simp add: ring_distribs)
    1.16    apply (rule mult_left_mono)
    1.17 -  apply (simp add: order_less_le)
    1.18 -  apply (simp add: order_less_le)
    1.19 -  apply (rule mult_left_mono)
    1.20    apply (rule abs_triangle_ineq)
    1.21    apply (simp add: order_less_le)
    1.22    apply (rule mult_nonneg_nonneg)
isabelle