--- a/src/HOL/Prod.thy Thu Mar 23 15:39:13 1995 +0100
+++ b/src/HOL/Prod.thy Fri Mar 24 12:30:35 1995 +0100
@@ -35,20 +35,19 @@
Sigma :: "['a set, 'a => 'b set] => ('a * 'b) set"
syntax
- "@Tuple" :: "args => 'a * 'b" ("(1<_>)")
+ "@Tuple" :: "['a, args] => 'a * 'b" ("(1'(_,/ _'))")
translations
- "<x, y, z>" == "<x, <y, z>>"
- "<x, y>" == "Pair x y"
- "<x>" => "x"
+ "(x, y, z)" == "(x, (y, z))"
+ "(x, y)" == "Pair x y"
defs
Pair_def "Pair a b == Abs_Prod(Pair_Rep a b)"
- fst_def "fst(p) == @a. ? b. p = <a, b>"
- snd_def "snd(p) == @b. ? a. p = <a, b>"
+ fst_def "fst(p) == @a. ? b. p = (a, b)"
+ snd_def "snd(p) == @b. ? a. p = (a, b)"
split_def "split c p == c (fst p) (snd p)"
- prod_fun_def "prod_fun f g == split(%x y.<f(x), g(y)>)"
- Sigma_def "Sigma A B == UN x:A. UN y:B(x). {<x, y>}"
+ prod_fun_def "prod_fun f g == split(%x y.(f(x), g(y)))"
+ Sigma_def "Sigma A B == UN x:A. UN y:B(x). {(x, y)}"
@@ -58,9 +57,9 @@
unit = "{p. p = True}"
consts
- Unity :: "unit" ("'(')")
+ "()" :: "unit" ("'(')")
defs
- Unity_def "Unity == Abs_Unit(True)"
+ Unity_def "() == Abs_Unit(True)"
end