src/HOL/SEQ.thy
changeset 37887 2ae085b07f2f
parent 37767 a2b7a20d6ea3
child 40811 ab0a8cc7976a
     1.1 --- a/src/HOL/SEQ.thy	Mon Jul 19 16:09:44 2010 +0200
     1.2 +++ b/src/HOL/SEQ.thy	Mon Jul 19 16:09:44 2010 +0200
     1.3 @@ -506,8 +506,7 @@
     1.4        from this obtain no where "\<forall>n\<ge>no. \<bar>f n - lim f\<bar> < lim f - x"
     1.5          by blast
     1.6        thus "lim f \<le> x"
     1.7 -        by (metis add_cancel_end add_minus_cancel diff_def linorder_linear 
     1.8 -                  linorder_not_le minus_diff_eq abs_diff_less_iff fn_le) 
     1.9 +        by (metis 1 LIMSEQ_le_const2 fn_le)
    1.10      qed
    1.11  qed
    1.12  
    1.13 @@ -971,7 +970,7 @@
    1.14  apply (rule_tac x = K in exI, simp)
    1.15  apply (rule exI [where x = 0], auto)
    1.16  apply (erule order_less_le_trans, simp)
    1.17 -apply (drule_tac x=n in spec, fold diff_def)
    1.18 +apply (drule_tac x=n in spec, fold diff_minus)
    1.19  apply (drule order_trans [OF norm_triangle_ineq2])
    1.20  apply simp
    1.21  done