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