src/HOLCF/Sprod0.thy
changeset 2291 fbd14a05fb88
parent 2278 d63ffafce255
child 2394 91d8abf108be
     1.1 --- a/src/HOLCF/Sprod0.thy	Mon Dec 02 12:19:56 1996 +0100
     1.2 +++ b/src/HOLCF/Sprod0.thy	Mon Dec 02 12:37:15 1996 +0100
     1.3 @@ -51,14 +51,6 @@
     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