diff -r 427106657e04 -r 9f6ed6840e8d src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Tue Oct 12 05:25:21 2010 -0700
+++ b/src/HOLCF/Cont.thy	Tue Oct 12 05:48:15 2010 -0700
@@ -22,12 +22,6 @@
   monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"  -- "monotonicity"  where
   "monofun f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
 
-(*
-definition
-  contlub :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool"  -- "first cont. def" where
-  "contlub f = (\<forall>Y. chain Y \<longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i)))"
-*)
-
 definition
   cont :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool"
 where
@@ -176,6 +170,17 @@
   "\<lbrakk>cont c; cont (\<lambda>x. f x)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. c (f x))"
 by (rule cont_apply [OF _ _ cont_const])
 
+text {* Least upper bounds preserve continuity *}
+
+lemma cont2cont_lub [simp]:
+  assumes chain: "\<And>x. chain (\<lambda>i. F i x)" and cont: "\<And>i. cont (\<lambda>x. F i x)"
+  shows "cont (\<lambda>x. \<Squnion>i. F i x)"
+apply (rule contI2)
+apply (simp add: monofunI cont2monofunE [OF cont] lub_mono chain)
+apply (simp add: cont2contlubE [OF cont])
+apply (simp add: diag_lub ch2ch_cont [OF cont] chain)
+done
+
 text {* if-then-else is continuous *}
 
 lemma cont_if [simp, cont2cont]: