src/HOL/Log.thy
changeset 50322 b06b95a5fda2
parent 50247 491c5c81c2e8
child 50346 a75c6429c3c3
     1.1 --- a/src/HOL/Log.thy	Mon Dec 03 18:13:23 2012 +0100
     1.2 +++ b/src/HOL/Log.thy	Mon Dec 03 18:18:59 2012 +0100
     1.3 @@ -364,7 +364,7 @@
     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: filter_lim_at_top)
     1.8 +  from assms have "eventually (\<lambda>x. Z < f x) F" by (simp add: filterlim_at_top)
     1.9    moreover
    1.10    from assms have "\<And>x. Z < x \<Longrightarrow> x powr s < Z powr s"
    1.11      by (auto simp: Z_def intro!: powr_less_mono2_neg)