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