src/HOL/Lim.thy
changeset 31017 2c227493ea56
parent 30273 ecd6f0ca62ea
child 31336 e17f13cd1280
     1.1 --- a/src/HOL/Lim.thy	Tue Apr 28 15:50:30 2009 +0200
     1.2 +++ b/src/HOL/Lim.thy	Tue Apr 28 15:50:30 2009 +0200
     1.3 @@ -383,7 +383,7 @@
     1.4  lemmas LIM_of_real = of_real.LIM
     1.5  
     1.6  lemma LIM_power:
     1.7 -  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{recpower,real_normed_algebra}"
     1.8 +  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{power,real_normed_algebra}"
     1.9    assumes f: "f -- a --> l"
    1.10    shows "(\<lambda>x. f x ^ n) -- a --> l ^ n"
    1.11  by (induct n, simp, simp add: LIM_mult f)
    1.12 @@ -530,7 +530,7 @@
    1.13    unfolding isCont_def by (rule LIM_of_real)
    1.14  
    1.15  lemma isCont_power:
    1.16 -  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{recpower,real_normed_algebra}"
    1.17 +  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{power,real_normed_algebra}"
    1.18    shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
    1.19    unfolding isCont_def by (rule LIM_power)
    1.20