# HG changeset patch
# User huffman
# Date 1148428045 -7200
# Node ID 78cd5f6af8e8df9e2fdf0e02fcf9ba1d27a44fcd
# Parent  a508bde37a81a9927ef216534e14540d5111030f
add theorem cfcomp_strict

diff -r a508bde37a81 -r 78cd5f6af8e8 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.