src/HOL/Analysis/Summation_Tests.thy

   fixes f :: "nat \<Rightarrow> 'a :: {banach,real_normed_div_algebra}"
   assumes nz:  "eventually (\<lambda>n. f n \<noteq> 0) sequentially"
   assumes lim: "(\<lambda>n. ereal (norm (f n) / norm (f (Suc n)))) \<longlonglongrightarrow> c"
   shows   "conv_radius f = c"
 proof (rule conv_radius_eqI')
-  show "c \<ge> 0" by (intro Lim_bounded2_ereal[OF lim]) simp_all
+  show "c \<ge> 0" by (intro Lim_bounded2[OF lim]) simp_all
 next
   fix r assume r: "0 < r" "ereal r < c"
   let ?l = "liminf (\<lambda>n. ereal (norm (f n * of_real r ^ n) / norm (f (Suc n) * of_real r ^ Suc n)))"
   have "?l = liminf (\<lambda>n. ereal (norm (f n) / (norm (f (Suc n)))) * ereal (inverse r))"
     using r by (simp add: norm_mult norm_power divide_simps)