src/HOL/Prod.thy

--- a/src/HOL/Prod.thy	Tue Apr 23 16:58:57 1996 +0200
+++ b/src/HOL/Prod.thy	Tue Apr 23 17:01:51 1996 +0200
@@ -83,17 +83,6 @@
   Unity_def     "() == Abs_Unit(True)"
 
 (* start 8bit 1 *)
-types
-
-('a, 'b) "ò"          (infixr 20)
-
-translations
-
-(type)  "x ò y"	== (type) "x * y" 
-
-  "³(x,y,zs).b"   == "split(³x.³(y,zs).b)"
-  "³(x,y).b"      == "split(³x y.b)"
-
 (* end 8bit 1 *)
 
 end