src/HOL/Prod.thy
changeset 1672 2c109cd2fdd0
parent 1660 8cb42cd97579
child 1674 33aff4d854e4
     1.1 --- a/src/HOL/Prod.thy	Tue Apr 23 16:44:22 1996 +0200
     1.2 +++ b/src/HOL/Prod.thy	Tue Apr 23 16:58:21 1996 +0200
     1.3 @@ -83,6 +83,17 @@
     1.4    Unity_def     "() == Abs_Unit(True)"
     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 +  "(x,y,zs).b"   == "split(x.(y,zs).b)"
    1.16 +  "(x,y).b"      == "split(x y.b)"
    1.17 +
    1.18  (* end 8bit 1 *)
    1.19  
    1.20  end