equal
deleted
inserted
replaced
69 "" :: "case_syn => cases_syn" ("_") |
69 "" :: "case_syn => cases_syn" ("_") |
70 "_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _") |
70 "_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _") |
71 |
71 |
72 translations |
72 translations |
73 "x ~= y" == "~ (x = y)" |
73 "x ~= y" == "~ (x = y)" |
74 "THE x. P" == "The (%x. P)" |
74 "THE x. P" => "The (%x. P)" |
75 "_Let (_binds b bs) e" == "_Let b (_Let bs e)" |
75 "_Let (_binds b bs) e" == "_Let b (_Let bs e)" |
76 "let x = a in e" == "Let a (%x. e)" |
76 "let x = a in e" == "Let a (%x. e)" |
|
77 |
|
78 print_translation {* |
|
79 (* To avoid eta-contraction of body: *) |
|
80 [("The", fn [Abs abs] => |
|
81 let val (x,t) = atomic_abs_tr' abs |
|
82 in Syntax.const "_The" $ x $ t end)] |
|
83 *} |
77 |
84 |
78 syntax (output) |
85 syntax (output) |
79 "=" :: "['a, 'a] => bool" (infix 50) |
86 "=" :: "['a, 'a] => bool" (infix 50) |
80 "_not_equal" :: "['a, 'a] => bool" (infix "~=" 50) |
87 "_not_equal" :: "['a, 'a] => bool" (infix "~=" 50) |
81 |
88 |