src/HOL/Prod.thy

--- a/src/HOL/Prod.thy	Tue Apr 23 16:44:22 1996 +0200
+++ b/src/HOL/Prod.thy	Tue Apr 23 16:58:21 1996 +0200
@@ -83,6 +83,17 @@
   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