diff -r 0774e9bcdb6c -r aa36d41e4263 src/HOLCF/Cprod.thy
--- a/src/HOLCF/Cprod.thy	Thu Jun 23 21:27:23 2005 +0200
+++ b/src/HOLCF/Cprod.thy	Thu Jun 23 22:07:30 2005 +0200
@@ -301,7 +301,7 @@
 lemma csplit2 [simp]: "csplit\<cdot>f\<cdot><x,y> = f\<cdot>x\<cdot>y"
 by (simp add: csplit_def)
 
-lemma csplit3: "csplit\<cdot>cpair\<cdot>z = z"
+lemma csplit3 [simp]: "csplit\<cdot>cpair\<cdot>z = z"
 by (simp add: csplit_def surjective_pairing_Cprod2)
 
 lemmas Cprod_rews = cfst_cpair csnd_cpair csplit2