src/HOLCF/Cfun.thy

--- 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)