50 |
50 |
51 "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" 10) |
51 "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3SIGMA _:_./ _)" 10) |
52 "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ Times _" [81, 80] 80) |
52 "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ Times _" [81, 80] 80) |
53 |
53 |
54 translations |
54 translations |
55 "(x, y, z)" == "(x, (y, z))" |
55 "(x, y, z)" == "(x, (y, z))" |
56 "(x, y)" == "Pair x y" |
56 "(x, y)" == "Pair x y" |
57 |
57 |
58 "%(x,y,zs).b" == "split(%x (y,zs).b)" |
58 "%(x,y,zs).b" == "split(%x (y,zs).b)" |
59 "%(x,y).b" == "split(%x y.b)" |
59 "%(x,y).b" == "split(%x y. b)" |
60 "_abs (Pair x y) t" => "%(x,y).t" |
60 "_abs (Pair x y) t" => "%(x,y).t" |
61 (* The last rule accommodates tuples in `case C ... (x,y) ... => ...' |
61 (* The last rule accommodates tuples in `case C ... (x,y) ... => ...' |
62 The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *) |
62 The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *) |
63 |
63 |
64 "SIGMA x:A.B" => "Sigma A (%x.B)" |
64 "SIGMA x:A. B" => "Sigma A (%x. B)" |
65 "A Times B" => "Sigma A (_K B)" |
65 "A Times B" => "Sigma A (_K B)" |
66 |
66 |
67 syntax (symbols) |
67 syntax (symbols) |
68 "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3\\<Sigma> _\\<in>_./ _)" 10) |
68 "@Sigma" :: "[pttrn, 'a set, 'b set] => ('a * 'b) set" ("(3\\<Sigma> _\\<in>_./ _)" 10) |
69 "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \\<times> _" [81, 80] 80) |
69 "@Times" :: "['a set, 'a => 'b set] => ('a * 'b) set" ("_ \\<times> _" [81, 80] 80) |
70 |
70 |