src/HOLCF/Cfun.thy

     \<Longrightarrow> (\<Lambda> x. \<Squnion>i. F i x) = (\<Squnion>i. \<Lambda> x. F i x)"
 apply (simp add: thelub_CFun)
 apply (simp add: Abs_CFun_inverse2)
 apply (simp add: thelub_fun ch2ch_lambda)
 done
+
+lemmas lub_distribs = 
+  contlub_cfun [symmetric]
+  contlub_LAM [symmetric]
 
 text {* strictness *}
 
 lemma strictI: "f\<cdot>x = \<bottom> \<Longrightarrow> f\<cdot>\<bottom> = \<bottom>"
 apply (rule UU_I)