src/HOL/Log.thy
changeset 50346 a75c6429c3c3
parent 50322 b06b95a5fda2
child 51478 270b21f3ae0a
     1.1 --- a/src/HOL/Log.thy	Tue Dec 04 16:20:24 2012 +0100
     1.2 +++ b/src/HOL/Log.thy	Tue Dec 04 18:00:31 2012 +0100
     1.3 @@ -364,7 +364,8 @@
     1.4  proof (rule tendstoI)
     1.5    fix e :: real assume "0 < e"
     1.6    def Z \<equiv> "e powr (1 / s)"
     1.7 -  from assms have "eventually (\<lambda>x. Z < f x) F" by (simp add: filterlim_at_top)
     1.8 +  from assms have "eventually (\<lambda>x. Z < f x) F"
     1.9 +    by (simp add: filterlim_at_top_dense)
    1.10    moreover
    1.11    from assms have "\<And>x. Z < x \<Longrightarrow> x powr s < Z powr s"
    1.12      by (auto simp: Z_def intro!: powr_less_mono2_neg)