author | huffman |
Mon, 14 Jan 2008 18:25:20 +0100 | |
changeset 25901 | bb178c8251e0 |
parent 25900 | 464f23aa905f |
child 25902 | c00823ce7288 |
--- 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>"