src/HOL/Library/Continuity.thy
changeset 32960 69916a850301
parent 32456 341c83339aeb
child 44928 7ef6505bde7f
     1.1 --- a/src/HOL/Library/Continuity.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Library/Continuity.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -67,11 +67,11 @@
     1.4      have "chain(%i. (F ^^ i) bot)"
     1.5      proof -
     1.6        { fix i have "(F ^^ i) bot \<le> (F ^^ (Suc i)) bot"
     1.7 -	proof (induct i)
     1.8 -	  case 0 show ?case by simp
     1.9 -	next
    1.10 -	  case Suc thus ?case using monoD[OF mono Suc] by auto
    1.11 -	qed }
    1.12 +        proof (induct i)
    1.13 +          case 0 show ?case by simp
    1.14 +        next
    1.15 +          case Suc thus ?case using monoD[OF mono Suc] by auto
    1.16 +        qed }
    1.17        thus ?thesis by(auto simp add:chain_def)
    1.18      qed
    1.19      hence "F ?U = (SUP i. (F ^^ (i+1)) bot)" using `continuous F` by (simp add:continuous_def)