src/HOLCF/Sprod0.thy
changeset 2278 d63ffafce255
parent 1479 21eb5e156d91
child 2291 fbd14a05fb88
     1.1 --- a/src/HOLCF/Sprod0.thy	Fri Nov 29 12:17:30 1996 +0100
     1.2 +++ b/src/HOLCF/Sprod0.thy	Fri Nov 29 12:22:22 1996 +0100
     1.3 @@ -51,6 +51,14 @@
     1.4                  &(! a b. ~a=UU & ~b=UU & p=Ispair a b    --> z=b)"  
     1.5  
     1.6  (* start 8bit 1 *)
     1.7 +types
     1.8 +
     1.9 +('a, 'b) "õ"          (infixr 20)
    1.10 +
    1.11 +translations
    1.12 +
    1.13 +(type)  "x õ y"	== (type) "x ** y" 
    1.14 +
    1.15  (* end 8bit 1 *)
    1.16  
    1.17  end