author haftmann Fri Apr 24 18:01:39 2009 +0200 (2009-04-24) changeset 30974 415f2fe37f62 parent 30973 304ab57afa6e child 30975 b2fa60d56735
removed confusion around funpow
```     1.1 --- a/src/HOL/Library/Topology_Euclidean_Space.thy	Fri Apr 24 17:45:17 2009 +0200
1.2 +++ b/src/HOL/Library/Topology_Euclidean_Space.thy	Fri Apr 24 18:01:39 2009 +0200
1.3 @@ -5441,7 +5441,7 @@
1.4    have "1 - c > 0" using c by auto
1.5
1.6    from s(2) obtain z0 where "z0 \<in> s" by auto
1.7 -  def z \<equiv> "\<lambda> n::nat. funpow n f z0"
1.8 +  def z \<equiv> "\<lambda>n. (f ^^ n) z0"
1.9    { fix n::nat
1.10      have "z n \<in> s" unfolding z_def
1.11      proof(induct n) case 0 thus ?case using `z0 \<in>s` by auto
1.12 @@ -5580,7 +5580,7 @@
1.13        using dist[THEN bspec[where x=x], THEN bspec[where x=y]] by auto } note dist' = this
1.14    def y \<equiv> "g x"
1.15    have [simp]:"y\<in>s" unfolding y_def using gs[unfolded image_subset_iff] and `x\<in>s` by blast
1.16 -  def f \<equiv> "\<lambda> n. funpow n g"
1.17 +  def f \<equiv> "\<lambda>n. g ^^ n"
1.18    have [simp]:"\<And>n z. g (f n z) = f (Suc n) z" unfolding f_def by auto
1.19    have [simp]:"\<And>z. f 0 z = z" unfolding f_def by auto
1.20    { fix n::nat and z assume "z\<in>s"
```