| changeset 25131 | 2c8caac48ade |
| parent 18078 | 20e5a6440790 |
| child 25135 | 4f8176c940cf |
--- a/src/HOLCF/Sprod.thy Sun Oct 21 14:21:45 2007 +0200 +++ b/src/HOLCF/Sprod.thy Sun Oct 21 14:21:48 2007 +0200 @@ -48,10 +48,10 @@ translations "(:x, y, z:)" == "(:x, (:y, z:):)" - "(:x, y:)" == "spair\<cdot>x\<cdot>y" + "(:x, y:)" == "CONST spair\<cdot>x\<cdot>y" translations - "\<Lambda>(spair\<cdot>x\<cdot>y). t" == "ssplit\<cdot>(\<Lambda> x y. t)" + "\<Lambda>(CONST spair\<cdot>x\<cdot>y). t" == "CONST ssplit\<cdot>(\<Lambda> x y. t)" subsection {* Case analysis *}