# HG changeset patch
# User huffman
# Date 1200359881 -3600
# Node ID e1b6521c1f94674ede88e66942345ebfbe672998
# Parent  a1a3f614dd8673701058a3a6c5889e51f471117d
declare cpair_strict [simp]

diff -r a1a3f614dd86 -r e1b6521c1f94 src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Mon Jan 14 23:19:28 2008 +0100
+++ b/src/HOLCF/Cprod.thy	Tue Jan 15 02:18:01 2008 +0100
@@ -245,7 +245,7 @@
 lemma cpair_defined_iff [iff]: "(<x, y> = \<bottom>) = (x = \<bottom> \<and> y = \<bottom>)"
 by (simp add: inst_cprod_pcpo cpair_eq_pair)
 
-lemma cpair_strict: "<\<bottom>, \<bottom>> = \<bottom>"
+lemma cpair_strict [simp]: "\<langle>\<bottom>, \<bottom>\<rangle> = \<bottom>"
 by simp
 
 lemma inst_cprod_pcpo2: "\<bottom> = <\<bottom>, \<bottom>>"
@@ -268,10 +268,10 @@
 by (simp add: cpair_eq_pair csnd_def cont_snd)
 
 lemma cfst_strict [simp]: "cfst\<cdot>\<bottom> = \<bottom>"
-by (simp add: inst_cprod_pcpo2)
+unfolding inst_cprod_pcpo2 by (rule cfst_cpair)
 
 lemma csnd_strict [simp]: "csnd\<cdot>\<bottom> = \<bottom>"
-by (simp add: inst_cprod_pcpo2)
+unfolding inst_cprod_pcpo2 by (rule csnd_cpair)
 
 lemma cpair_cfst_csnd: "\<langle>cfst\<cdot>p, csnd\<cdot>p\<rangle> = p"
 by (cases p rule: cprodE, simp)