equal
deleted
inserted
replaced
44 Let :: "['a, 'a => 'b] => 'b" |
44 Let :: "['a, 'a => 'b] => 'b" |
45 "@Let" :: "[idt, 'a, 'b] => 'b" ("(let _ = (2_)/ in (2_))" 10) |
45 "@Let" :: "[idt, 'a, 'b] => 'b" ("(let _ = (2_)/ in (2_))" 10) |
46 |
46 |
47 (* Alternative Quantifiers *) |
47 (* Alternative Quantifiers *) |
48 |
48 |
49 "*The" :: "[idts, bool] => 'a" ("(3THE _./ _)" 10) |
|
50 "*All" :: "[idts, bool] => bool" ("(3ALL _./ _)" 10) |
49 "*All" :: "[idts, bool] => bool" ("(3ALL _./ _)" 10) |
51 "*Ex" :: "[idts, bool] => bool" ("(3EX _./ _)" 10) |
50 "*Ex" :: "[idts, bool] => bool" ("(3EX _./ _)" 10) |
52 "*Ex1" :: "[idts, bool] => bool" ("(3EX! _./ _)" 10) |
51 "*Ex1" :: "[idts, bool] => bool" ("(3EX! _./ _)" 10) |
53 |
52 |
54 (* Infixes *) |
53 (* Infixes *) |
65 "-" :: "['a::minus, 'a] => 'a" (infixl 65) |
64 "-" :: "['a::minus, 'a] => 'a" (infixl 65) |
66 "*" :: "['a::times, 'a] => 'a" (infixl 70) |
65 "*" :: "['a::times, 'a] => 'a" (infixl 70) |
67 |
66 |
68 |
67 |
69 translations |
68 translations |
70 "THE xs. P" => "@ xs. P" |
|
71 "ALL xs. P" => "! xs. P" |
69 "ALL xs. P" => "! xs. P" |
72 "EX xs. P" => "? xs. P" |
70 "EX xs. P" => "? xs. P" |
73 "EX! xs. P" => "?! xs. P" |
71 "EX! xs. P" => "?! xs. P" |
74 |
72 |
75 "x ~= y" == "~ (x=y)" |
73 "x ~= y" == "~ (x=y)" |
131 (name, ast_tr') |
129 (name, ast_tr') |
132 end; |
130 end; |
133 |
131 |
134 |
132 |
135 val print_ast_translation = |
133 val print_ast_translation = |
136 map alt_ast_tr' [("@", "*The"), ("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")]; |
134 map alt_ast_tr' [("! ", "*All"), ("? ", "*Ex"), ("?! ", "*Ex1")]; |
137 |
135 |