src/HOL/Log.thy
changeset 50247 491c5c81c2e8
parent 49962 a8cc904a6820
child 50322 b06b95a5fda2
     1.1 --- a/src/HOL/Log.thy	Tue Nov 27 13:48:40 2012 +0100
     1.2 +++ b/src/HOL/Log.thy	Tue Nov 27 19:31:11 2012 +0100
     1.3 @@ -359,12 +359,12 @@
     1.4  qed
     1.5  
     1.6  lemma tendsto_neg_powr:
     1.7 -  assumes "s < 0" and "real_tendsto_inf f F"
     1.8 +  assumes "s < 0" and "LIM x F. f x :> at_top"
     1.9    shows "((\<lambda>x. f x powr s) ---> 0) F"
    1.10  proof (rule tendstoI)
    1.11    fix e :: real assume "0 < e"
    1.12    def Z \<equiv> "e powr (1 / s)"
    1.13 -  from assms have "eventually (\<lambda>x. Z < f x) F" by (simp add: real_tendsto_inf_def)
    1.14 +  from assms have "eventually (\<lambda>x. Z < f x) F" by (simp add: filter_lim_at_top)
    1.15    moreover
    1.16    from assms have "\<And>x. Z < x \<Longrightarrow> x powr s < Z powr s"
    1.17      by (auto simp: Z_def intro!: powr_less_mono2_neg)