# HG changeset patch
# User huffman
# Date 1287787663 25200
# Node ID c2d36bc4cd14a1733ce097e3dae81b417c31b47f
# Parent  baf5953615da000491f6487cc881263069644935
add lemma strict3

diff -r baf5953615da -r c2d36bc4cd14 src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Fri Oct 22 11:24:52 2010 -0700
+++ b/src/HOLCF/Cfun.thy	Fri Oct 22 15:47:43 2010 -0700
@@ -544,7 +544,10 @@
 lemma strict2 [simp]: "x \<noteq> \<bottom> \<Longrightarrow> strict\<cdot>x = ID"
 by (simp add: strict_conv_if)
 
- definition
+lemma strict3 [simp]: "strict\<cdot>x\<cdot>\<bottom> = \<bottom>"
+by (simp add: strict_conv_if)
+
+definition
   strictify  :: "('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'b" where
   "strictify = (\<Lambda> f x. strict\<cdot>x\<cdot>(f\<cdot>x))"
 
diff -r baf5953615da -r c2d36bc4cd14 src/HOLCF/Sprod.thy
--- a/src/HOLCF/Sprod.thy	Fri Oct 22 11:24:52 2010 -0700
+++ b/src/HOLCF/Sprod.thy	Fri Oct 22 15:47:43 2010 -0700
@@ -75,10 +75,10 @@
 subsection {* Properties of \emph{spair} *}
 
 lemma spair_strict1 [simp]: "(:\<bottom>, y:) = \<bottom>"
-by (simp add: Rep_Sprod_simps strict_conv_if)
+by (simp add: Rep_Sprod_simps)
 
 lemma spair_strict2 [simp]: "(:x, \<bottom>:) = \<bottom>"
-by (simp add: Rep_Sprod_simps strict_conv_if)
+by (simp add: Rep_Sprod_simps)
 
 lemma spair_strict_iff [simp]: "((:x, y:) = \<bottom>) = (x = \<bottom> \<or> y = \<bottom>)"
 by (simp add: Rep_Sprod_simps strict_conv_if)