Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Lim.thy
changeset 31017 2c227493ea56
parent 30273 ecd6f0ca62ea
child 31336 e17f13cd1280 
--- a/src/HOL/Lim.thy	Tue Apr 28 15:50:30 2009 +0200
+++ b/src/HOL/Lim.thy	Tue Apr 28 15:50:30 2009 +0200
@@ -383,7 +383,7 @@
 lemmas LIM_of_real = of_real.LIM
 
 lemma LIM_power:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{recpower,real_normed_algebra}"
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{power,real_normed_algebra}"
   assumes f: "f -- a --> l"
   shows "(\<lambda>x. f x ^ n) -- a --> l ^ n"
 by (induct n, simp, simp add: LIM_mult f)
@@ -530,7 +530,7 @@
   unfolding isCont_def by (rule LIM_of_real)
 
 lemma isCont_power:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{recpower,real_normed_algebra}"
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::{power,real_normed_algebra}"
   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
   unfolding isCont_def by (rule LIM_power)
isabelle