src/HOLCF/Cfun.thy

--- a/src/HOLCF/Cfun.thy	Wed May 24 01:05:02 2006 +0200
+++ b/src/HOLCF/Cfun.thy	Wed May 24 01:47:25 2006 +0200
@@ -456,6 +456,9 @@
 lemma cfcomp2 [simp]: "(f oo g)\<cdot>x = f\<cdot>(g\<cdot>x)"
 by (simp add: cfcomp1)
 
+lemma cfcomp_strict [simp]: "\<bottom> oo f = \<bottom>"
+by (simp add: expand_cfun_eq)
+
 text {*
   Show that interpretation of (pcpo,@{text "_->_"}) is a category.
   The class of objects is interpretation of syntactical class pcpo.