--- a/src/HOLCF/Cprod.thy Mon Nov 02 13:43:50 2009 -0800
+++ b/src/HOLCF/Cprod.thy Mon Nov 02 17:19:49 2009 -0800
@@ -52,6 +52,7 @@
translations
"\<Lambda>(CONST cpair\<cdot>x\<cdot>y). t" == "CONST csplit\<cdot>(\<Lambda> x y. t)"
+ "\<Lambda>(CONST Pair x y). t" => "CONST csplit\<cdot>(\<Lambda> x y. t)"
subsection {* Convert all lemmas to the continuous versions *}
@@ -150,6 +151,9 @@
lemma csplit3 [simp]: "csplit\<cdot>cpair\<cdot>z = z"
by (simp add: csplit_def cpair_cfst_csnd)
+lemma csplit_Pair [simp]: "csplit\<cdot>f\<cdot>(x, y) = f\<cdot>x\<cdot>y"
+by (simp add: csplit_def cfst_def csnd_def)
+
lemmas Cprod_rews = cfst_cpair csnd_cpair csplit2
subsection {* Product type is a bifinite domain *}