src/HOL/Prod.thy
changeset 1558 9c6ebfab4e05
parent 1475 7f5a4cd08209
child 1636 e18416e3e1d4
     1.1 --- a/src/HOL/Prod.thy	Wed Mar 06 14:19:39 1996 +0100
     1.2 +++ b/src/HOL/Prod.thy	Fri Mar 08 13:11:09 1996 +0100
     1.3 @@ -13,11 +13,9 @@
     1.4  
     1.5  (* type definition *)
     1.6  
     1.7 -consts
     1.8 +constdefs
     1.9    Pair_Rep      :: ['a, 'b] => ['a, 'b] => bool
    1.10 -
    1.11 -defs
    1.12 -  Pair_Rep_def  "Pair_Rep == (%a b. %x y. x=a & y=b)"
    1.13 +  "Pair_Rep == (%a b. %x y. x=a & y=b)"
    1.14  
    1.15  typedef (Prod)
    1.16    ('a, 'b) "*"          (infixr 20)