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"
```