src/HOL/Log.thy

   assumes "s < 0" and "LIM x F. f x :> at_top"
   shows "((\<lambda>x. f x powr s) ---> 0) F"
 proof (rule tendstoI)
   fix e :: real assume "0 < e"
   def Z \<equiv> "e powr (1 / s)"
-  from assms have "eventually (\<lambda>x. Z < f x) F" by (simp add: filterlim_at_top)
+  from assms have "eventually (\<lambda>x. Z < f x) F"
+    by (simp add: filterlim_at_top_dense)
   moreover
   from assms have "\<And>x. Z < x \<Longrightarrow> x powr s < Z powr s"
     by (auto simp: Z_def intro!: powr_less_mono2_neg)
   with assms `0 < e` have "\<And>x. Z < x \<Longrightarrow> dist (x powr s) 0 < e"
     by (simp add: powr_powr Z_def dist_real_def)