src/HOL/Prod.thy
changeset 972 e61b058d58d2
parent 967 bfcb53497a99
child 1068 e0f2dffab506
     1.1 --- a/src/HOL/Prod.thy	Thu Mar 23 15:39:13 1995 +0100
     1.2 +++ b/src/HOL/Prod.thy	Fri Mar 24 12:30:35 1995 +0100
     1.3 @@ -35,20 +35,19 @@
     1.4    Sigma         :: "['a set, 'a => 'b set] => ('a * 'b) set"
     1.5  
     1.6  syntax
     1.7 -  "@Tuple"      :: "args => 'a * 'b"            ("(1<_>)")
     1.8 +  "@Tuple"      :: "['a, args] => 'a * 'b"            ("(1'(_,/ _'))")
     1.9  
    1.10  translations
    1.11 -  "<x, y, z>"   == "<x, <y, z>>"
    1.12 -  "<x, y>"      == "Pair x y"
    1.13 -  "<x>"         => "x"
    1.14 +  "(x, y, z)"   == "(x, (y, z))"
    1.15 +  "(x, y)"      == "Pair x y"
    1.16  
    1.17  defs
    1.18    Pair_def      "Pair a b == Abs_Prod(Pair_Rep a b)"
    1.19 -  fst_def       "fst(p) == @a. ? b. p = <a, b>"
    1.20 -  snd_def       "snd(p) == @b. ? a. p = <a, b>"
    1.21 +  fst_def       "fst(p) == @a. ? b. p = (a, b)"
    1.22 +  snd_def       "snd(p) == @b. ? a. p = (a, b)"
    1.23    split_def     "split c p == c (fst p) (snd p)"
    1.24 -  prod_fun_def  "prod_fun f g == split(%x y.<f(x), g(y)>)"
    1.25 -  Sigma_def     "Sigma A B == UN x:A. UN y:B(x). {<x, y>}"
    1.26 +  prod_fun_def  "prod_fun f g == split(%x y.(f(x), g(y)))"
    1.27 +  Sigma_def     "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
    1.28  
    1.29  
    1.30  
    1.31 @@ -58,9 +57,9 @@
    1.32    unit = "{p. p = True}"
    1.33  
    1.34  consts
    1.35 -  Unity         :: "unit"                       ("'(')")
    1.36 +  "()"          :: "unit"                           ("'(')")
    1.37  
    1.38  defs
    1.39 -  Unity_def     "Unity == Abs_Unit(True)"
    1.40 +  Unity_def     "() == Abs_Unit(True)"
    1.41  
    1.42  end