src/HOLCF/Cprod.thy
changeset 16553 aa36d41e4263
parent 16315 bfb2f513916a
child 16750 282d092b1dbd
     1.1 --- a/src/HOLCF/Cprod.thy	Thu Jun 23 21:27:23 2005 +0200
     1.2 +++ b/src/HOLCF/Cprod.thy	Thu Jun 23 22:07:30 2005 +0200
     1.3 @@ -301,7 +301,7 @@
     1.4  lemma csplit2 [simp]: "csplit\<cdot>f\<cdot><x,y> = f\<cdot>x\<cdot>y"
     1.5  by (simp add: csplit_def)
     1.6  
     1.7 -lemma csplit3: "csplit\<cdot>cpair\<cdot>z = z"
     1.8 +lemma csplit3 [simp]: "csplit\<cdot>cpair\<cdot>z = z"
     1.9  by (simp add: csplit_def surjective_pairing_Cprod2)
    1.10  
    1.11  lemmas Cprod_rews = cfst_cpair csnd_cpair csplit2