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)