src/HOLCF/Sprod.thy
changeset 25131 2c8caac48ade
parent 18078 20e5a6440790
child 25135 4f8176c940cf
     1.1 --- a/src/HOLCF/Sprod.thy	Sun Oct 21 14:21:45 2007 +0200
     1.2 +++ b/src/HOLCF/Sprod.thy	Sun Oct 21 14:21:48 2007 +0200
     1.3 @@ -48,10 +48,10 @@
     1.4  
     1.5  translations
     1.6    "(:x, y, z:)" == "(:x, (:y, z:):)"
     1.7 -  "(:x, y:)"    == "spair\<cdot>x\<cdot>y"
     1.8 +  "(:x, y:)"    == "CONST spair\<cdot>x\<cdot>y"
     1.9  
    1.10  translations
    1.11 -  "\<Lambda>(spair\<cdot>x\<cdot>y). t" == "ssplit\<cdot>(\<Lambda> x y. t)"
    1.12 +  "\<Lambda>(CONST spair\<cdot>x\<cdot>y). t" == "CONST ssplit\<cdot>(\<Lambda> x y. t)"
    1.13  
    1.14  subsection {* Case analysis *}
    1.15