--- 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)