src/HOLCF/Sprod3.thy
changeset 442 13ac1fd0a14d
parent 243 c22b85994e17
child 625 119391dd1d59
     1.1 --- a/src/HOLCF/Sprod3.thy	Wed Jun 29 12:01:17 1994 +0200
     1.2 +++ b/src/HOLCF/Sprod3.thy	Wed Jun 29 12:03:41 1994 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4  
     1.5  rules 
     1.6  
     1.7 -inst_sprod_pcpo	"UU::'a**'b = Ispair(UU,UU)"
     1.8 +inst_sprod_pcpo	"(UU::'a**'b) = Ispair(UU,UU)"
     1.9  spair_def	"spair  == (LAM x y.Ispair(x,y))"
    1.10  sfst_def	"sfst   == (LAM p.Isfst(p))"
    1.11  ssnd_def	"ssnd   == (LAM p.Issnd(p))"