author | huffman |
Thu, 19 Jun 2008 20:34:28 +0200 | |
changeset 27274 | 1c97c471db82 |
parent 27273 | d54ae0bdad80 |
child 27275 | f54aa7c4ff32 |
--- a/src/HOLCF/Cfun.thy Thu Jun 19 17:32:18 2008 +0200 +++ b/src/HOLCF/Cfun.thy Thu Jun 19 20:34:28 2008 +0200 @@ -465,6 +465,9 @@ lemma cfcomp2 [simp]: "(f oo g)\<cdot>x = f\<cdot>(g\<cdot>x)" by (simp add: cfcomp1) +lemma cfcomp_LAM: "cont g \<Longrightarrow> f oo (\<Lambda> x. g x) = (\<Lambda> x. f\<cdot>(g x))" +by (simp add: cfcomp1) + lemma cfcomp_strict [simp]: "\<bottom> oo f = \<bottom>" by (simp add: expand_cfun_eq)