src/HOL/SEQ.thy
changeset 31017 2c227493ea56
parent 30730 4d3565f2cb0e
child 31336 e17f13cd1280
     1.1 --- a/src/HOL/SEQ.thy	Tue Apr 28 15:50:30 2009 +0200
     1.2 +++ b/src/HOL/SEQ.thy	Tue Apr 28 15:50:30 2009 +0200
     1.3 @@ -487,7 +487,7 @@
     1.4  by (simp add: LIMSEQ_mult LIMSEQ_inverse divide_inverse)
     1.5  
     1.6  lemma LIMSEQ_pow:
     1.7 -  fixes a :: "'a::{real_normed_algebra,recpower}"
     1.8 +  fixes a :: "'a::{power, real_normed_algebra}"
     1.9    shows "X ----> a \<Longrightarrow> (\<lambda>n. (X n) ^ m) ----> a ^ m"
    1.10  by (induct m) (simp_all add: LIMSEQ_const LIMSEQ_mult)
    1.11  
    1.12 @@ -1394,7 +1394,7 @@
    1.13  qed
    1.14  
    1.15  lemma LIMSEQ_power_zero:
    1.16 -  fixes x :: "'a::{real_normed_algebra_1,recpower}"
    1.17 +  fixes x :: "'a::{real_normed_algebra_1}"
    1.18    shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
    1.19  apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero])
    1.20  apply (simp only: LIMSEQ_Zseq_iff, erule Zseq_le)