src/HOL/Prod.thy
changeset 1674 33aff4d854e4
parent 1672 2c109cd2fdd0
child 1755 17001ecd546e
     1.1 --- a/src/HOL/Prod.thy	Tue Apr 23 16:58:57 1996 +0200
     1.2 +++ b/src/HOL/Prod.thy	Tue Apr 23 17:01:51 1996 +0200
     1.3 @@ -83,17 +83,6 @@
     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