# HG changeset patch
# User haftmann
# Date 1240588899 -7200
# Node ID 415f2fe37f62b5b70c677b84b6e5db6b2ff7c9b6
# Parent  304ab57afa6ecacc354937517a5c18abb729a8d0
removed confusion around funpow

diff -r 304ab57afa6e -r 415f2fe37f62 src/HOL/Library/Topology_Euclidean_Space.thy
--- a/src/HOL/Library/Topology_Euclidean_Space.thy	Fri Apr 24 17:45:17 2009 +0200
+++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Fri Apr 24 18:01:39 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. funpow n f z0"
+  def z \<equiv> "\<lambda>n. (f ^^ n) 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. funpow n g"
+  def f \<equiv> "\<lambda>n. g ^^ n"
   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"