src/HOL/Transcendental.thy
changeset 51641 cd05e9fcc63d
parent 51527 bd62e7ff103b
child 52139 40fe6b80b481
     1.1 --- a/src/HOL/Transcendental.thy	Mon Apr 08 21:01:59 2013 +0200
     1.2 +++ b/src/HOL/Transcendental.thy	Tue Apr 09 14:04:41 2013 +0200
     1.3 @@ -1578,7 +1578,7 @@
     1.4  
     1.5  lemma ln_at_0: "LIM x at_right 0. ln x :> at_bot"
     1.6    by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
     1.7 -     (auto simp: eventually_within)
     1.8 +     (auto simp: eventually_at_filter)
     1.9  
    1.10  lemma ln_at_top: "LIM x at_top. ln x :> at_top"
    1.11    by (rule filterlim_at_top_at_top[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
    1.12 @@ -3190,12 +3190,12 @@
    1.13  
    1.14  lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- pi/2))"
    1.15    by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
    1.16 -     (auto simp: le_less eventually_within_less dist_real_def simp del: less_divide_eq_numeral1
    1.17 +     (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
    1.18             intro!: tan_monotone exI[of _ "pi/2"])
    1.19  
    1.20  lemma filterlim_tan_at_left: "filterlim tan at_top (at_left (pi/2))"
    1.21    by (rule filterlim_at_top_at_left[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
    1.22 -     (auto simp: le_less eventually_within_less dist_real_def simp del: less_divide_eq_numeral1
    1.23 +     (auto simp: le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1
    1.24             intro!: tan_monotone exI[of _ "pi/2"])
    1.25  
    1.26  lemma tendsto_arctan_at_top: "(arctan ---> (pi/2)) at_top"