--- a/src/HOL/Library/Topology_Euclidean_Space.thy Fri Apr 17 16:41:31 2009 +0200
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy Mon Apr 20 09:32:07 2009 +0200
@@ -5441,7 +5441,7 @@
have "1 - c > 0" using c by auto
from s(2) obtain z0 where "z0 \<in> s" by auto
- def z \<equiv> "\<lambda> n::nat. fun_pow n f z0"
+ def z \<equiv> "\<lambda> n::nat. funpow n f z0"
{ fix n::nat
have "z n \<in> s" unfolding z_def
proof(induct n) case 0 thus ?case using `z0 \<in>s` by auto
@@ -5580,7 +5580,7 @@
using dist[THEN bspec[where x=x], THEN bspec[where x=y]] by auto } note dist' = this
def y \<equiv> "g x"
have [simp]:"y\<in>s" unfolding y_def using gs[unfolded image_subset_iff] and `x\<in>s` by blast
- def f \<equiv> "\<lambda> n. fun_pow n g"
+ def f \<equiv> "\<lambda> n. funpow n g"
have [simp]:"\<And>n z. g (f n z) = f (Suc n) z" unfolding f_def by auto
have [simp]:"\<And>z. f 0 z = z" unfolding f_def by auto
{ fix n::nat and z assume "z\<in>s"