src/HOL/SEQ.thy

   fixes a b :: "'a::real_normed_field"
   shows "\<lbrakk>X ----> a; Y ----> b; b \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>n. X n / Y n) ----> a / b"
 by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse)
 
 lemma LIMSEQ_pow:
-  fixes a :: "'a::{real_normed_algebra,recpower}"
+  fixes a :: "'a::{power, real_normed_algebra}"
   shows "X ----> a \<Longrightarrow> (\<lambda>n. (X n) ^ m) ----> a ^ m"
 by (induct m) (simp_all add: LIMSEQ_const LIMSEQ_mult)
 
 lemma LIMSEQ_setsum:
   assumes n: "\<And>n. n \<in> S \<Longrightarrow> X n ----> L n"

     by (rule LIMSEQ_inverse_realpow_zero)
   thus ?thesis by (simp add: power_inverse)
 qed
 
 lemma LIMSEQ_power_zero:
-  fixes x :: "'a::{real_normed_algebra_1,recpower}"
+  fixes x :: "'a::{real_normed_algebra_1}"
   shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
 apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero])
 apply (simp only: LIMSEQ_Zseq_iff, erule Zseq_le)
 apply (simp add: power_abs norm_power_ineq)
 done