src/HOL/Prod.thy
changeset 1370 7361ac9b024d
parent 1273 6960ec882bca
child 1454 d0266c81a85e
     1.1 --- a/src/HOL/Prod.thy	Mon Nov 27 13:44:56 1995 +0100
     1.2 +++ b/src/HOL/Prod.thy	Wed Nov 29 16:44:59 1995 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4  (* type definition *)
     1.5  
     1.6  consts
     1.7 -  Pair_Rep      :: "['a, 'b] => ['a, 'b] => bool"
     1.8 +  Pair_Rep      :: ['a, 'b] => ['a, 'b] => bool
     1.9  
    1.10  defs
    1.11    Pair_Rep_def  "Pair_Rep == (%a b. %x y. x=a & y=b)"
    1.12 @@ -40,9 +40,9 @@
    1.13  syntax
    1.14    "@Tuple"      :: "['a, args] => 'a * 'b"            ("(1'(_,/ _'))")
    1.15  
    1.16 -  "@pttrn"  :: "[pttrn,pttrns] => pttrn"              ("'(_,/_')")
    1.17 -  ""        :: " pttrn         => pttrns"             ("_")
    1.18 -  "@pttrns" :: "[pttrn,pttrns] => pttrns"             ("_,/_")
    1.19 +  "@pttrn"  :: [pttrn,pttrns] => pttrn              ("'(_,/_')")
    1.20 +  ""        ::  pttrn         => pttrns             ("_")
    1.21 +  "@pttrns" :: [pttrn,pttrns] => pttrns             ("_,/_")
    1.22  
    1.23  translations
    1.24    "(x, y, z)"   == "(x, (y, z))"
    1.25 @@ -69,7 +69,7 @@
    1.26    unit = "{p. p = True}"
    1.27  
    1.28  consts
    1.29 -  "()"          :: "unit"                           ("'(')")
    1.30 +  "()"          :: unit                           ("'(')")
    1.31  
    1.32  defs
    1.33    Unity_def     "() == Abs_Unit(True)"