equal
deleted
inserted
replaced
127 "_case1" :: "['a, 'b] => case_syn" ("(2_ =>/ _)" 10) |
127 "_case1" :: "['a, 'b] => case_syn" ("(2_ =>/ _)" 10) |
128 "" :: "case_syn => cases_syn" ("_") |
128 "" :: "case_syn => cases_syn" ("_") |
129 "_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _") |
129 "_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ | _") |
130 |
130 |
131 translations |
131 translations |
132 "THE x. P" == "The (%x. P)" |
132 "THE x. P" == "CONST The (%x. P)" |
133 "_Let (_binds b bs) e" == "_Let b (_Let bs e)" |
133 "_Let (_binds b bs) e" == "_Let b (_Let bs e)" |
134 "let x = a in e" == "Let a (%x. e)" |
134 "let x = a in e" == "CONST Let a (%x. e)" |
135 |
135 |
136 print_translation {* |
136 print_translation {* |
137 (* To avoid eta-contraction of body: *) |
137 [(@{const_syntax The}, fn [Abs abs] => |
138 [("The", fn [Abs abs] => |
138 let val (x, t) = atomic_abs_tr' abs |
139 let val (x,t) = atomic_abs_tr' abs |
139 in Syntax.const @{syntax_const "_The"} $ x $ t end)] |
140 in Syntax.const "_The" $ x $ t end)] |
140 *} -- {* To avoid eta-contraction of body *} |
141 *} |
|
142 |
141 |
143 syntax (xsymbols) |
142 syntax (xsymbols) |
144 "_case1" :: "['a, 'b] => case_syn" ("(2_ \<Rightarrow>/ _)" 10) |
143 "_case1" :: "['a, 'b] => case_syn" ("(2_ \<Rightarrow>/ _)" 10) |
145 |
144 |
146 notation (xsymbols) |
145 notation (xsymbols) |