src/HOL/Library/Formal_Power_Series.thy

     }
     then have "\<exists>n0. \<forall> n \<ge> n0. dist (?s n) a < r"
       by blast
   }
   then show ?thesis
-    unfolding LIMSEQ_def by blast
+    unfolding lim_sequentially by blast
 qed
 
 
 subsection{* Inverses of formal power series *}