# HG changeset patch
# User huffman
# Date 1257211189 28800
# Node ID 768b2bb9e66ab7597f603ca3d19bbf7de46aed45
# Parent  609389f3ea1e427c1a477510fcd1d98185ca76d5
add (LAM (x, y). t) syntax and lemma csplit_Pair

diff -r 609389f3ea1e -r 768b2bb9e66a src/HOLCF/Cprod.thy
--- 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 *}