# HG changeset patch
# User huffman
# Date 1269323726 25200
# Node ID bfa52a972745326a1dadf833467fa4bcf31260eb
# Parent  cd1b0166481037bc96c4ef630aa17bbba2c12386
define csplit using fst, snd

diff -r cd1b01664810 -r bfa52a972745 src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Mon Mar 22 22:43:21 2010 -0700
+++ b/src/HOLCF/Cprod.thy	Mon Mar 22 22:55:26 2010 -0700
@@ -34,11 +34,11 @@
 
 definition
   csnd :: "('a * 'b) \<rightarrow> 'b" where
-  "csnd = (\<Lambda> p. snd p)"      
+  "csnd = (\<Lambda> p. snd p)"
 
 definition
   csplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a * 'b) \<rightarrow> 'c" where
-  "csplit = (\<Lambda> f p. f\<cdot>(cfst\<cdot>p)\<cdot>(csnd\<cdot>p))"
+  "csplit = (\<Lambda> f p. f\<cdot>(fst p)\<cdot>(snd p))"
 
 syntax
   "_ctuple" :: "['a, args] \<Rightarrow> 'a * 'b"  ("(1<_,/ _>)")
@@ -146,13 +146,13 @@
 by (simp add: csplit_def)
 
 lemma csplit2 [simp]: "csplit\<cdot>f\<cdot><x,y> = f\<cdot>x\<cdot>y"
-by (simp add: csplit_def)
+by (simp add: csplit_def cpair_def)
 
 lemma csplit3 [simp]: "csplit\<cdot>cpair\<cdot>z = z"
-by (simp add: csplit_def cpair_cfst_csnd)
+by (simp add: csplit_def cpair_def)
 
 lemma csplit_Pair [simp]: "csplit\<cdot>f\<cdot>(x, y) = f\<cdot>x\<cdot>y"
-by (simp add: csplit_def cfst_def csnd_def)
+by (simp add: csplit_def)
 
 lemmas Cprod_rews = cfst_cpair csnd_cpair csplit2