removed confusion around funpow
authorhaftmann
Fri Apr 24 18:01:39 2009 +0200 (2009-04-24)
changeset 30974415f2fe37f62
parent 30973 304ab57afa6e
child 30975 b2fa60d56735
removed confusion around funpow
src/HOL/Library/Topology_Euclidean_Space.thy
     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"