changeset 16553 | aa36d41e4263 |
parent 16315 | bfb2f513916a |
child 16750 | 282d092b1dbd |
--- 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