src/HOLCF/Sprod0.thy
changeset 2291 fbd14a05fb88
parent 2278 d63ffafce255
child 2394 91d8abf108be
--- a/src/HOLCF/Sprod0.thy	Mon Dec 02 12:19:56 1996 +0100
+++ b/src/HOLCF/Sprod0.thy	Mon Dec 02 12:37:15 1996 +0100
@@ -51,14 +51,6 @@
                 &(! a b. ~a=UU & ~b=UU & p=Ispair a b    --> z=b)"  
 
 (* start 8bit 1 *)
-types
-
-('a, 'b) "õ"          (infixr 20)
-
-translations
-
-(type)  "x õ y"	== (type) "x ** y" 
-
 (* end 8bit 1 *)
 
 end