# HG changeset patch
# User huffman
# Date 1200331520 -3600
# Node ID bb178c8251e0943c4e427b11ae10d53ec08d0e31
# Parent  464f23aa905ff3bf634a29816dd43cdc2092dcbe
added lemmas lub_distribs

diff -r 464f23aa905f -r bb178c8251e0 src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Mon Jan 14 16:15:55 2008 +0100
+++ b/src/HOLCF/Cfun.thy	Mon Jan 14 18:25:20 2008 +0100
@@ -252,6 +252,10 @@
 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>"