138 (** Pure syntax **) |
138 (** Pure syntax **) |
139 |
139 |
140 val pure_types = |
140 val pure_types = |
141 map (fn t => (t, 0, NoSyn)) |
141 map (fn t => (t, 0, NoSyn)) |
142 (terminals @ [logic, "type", "types", "sort", "classes", args, |
142 (terminals @ [logic, "type", "types", "sort", "classes", args, |
143 "idt", "idts", "aprop", "asms", any, sprop]); |
143 "pttrn", "idt", "idts", "aprop", "asms", any, sprop]); |
144 |
144 |
145 val pure_syntax = |
145 val pure_syntax = |
146 [("_lambda", "[idts, 'a] => logic", Mixfix ("(3%_./ _)", [], 0)), |
146 [("_lambda", "[idts, 'a] => logic", Mixfix ("(3%_./ _)", [], 0)), |
147 ("_abs", "'a", NoSyn), |
147 ("_abs", "'a", NoSyn), |
148 ("", "'a => " ^ args, Delimfix "_"), |
148 ("", "'a => " ^ args, Delimfix "_"), |
149 ("_args", "['a, " ^ args ^ "] => " ^ args, Delimfix "_,/ _"), |
149 ("_args", "['a, " ^ args ^ "] => " ^ args, Delimfix "_,/ _"), |
150 ("", "id => idt", Delimfix "_"), |
150 ("", "id => idt", Delimfix "_"), |
151 ("_idtyp", "[id, type] => idt", Mixfix ("_::_", [], 0)), |
151 ("_idtyp", "[id, type] => idt", Mixfix ("_::_", [], 0)), |
152 ("", "idt => idt", Delimfix "'(_')"), |
152 ("", "idt => idt", Delimfix "'(_')"), |
153 ("", "idt => idts", Delimfix "_"), |
153 ("", "idt => pttrn", Delimfix "_"), |
154 ("_idts", "[idt, idts] => idts", Mixfix ("_/ _", [1, 0], 0)), |
154 ("", "pttrn => idts", Delimfix "_"), |
|
155 ("_idts", "[pttrn, idts] => idts", Mixfix ("_/ _", [1, 0], 0)), |
155 ("", "id => aprop", Delimfix "_"), |
156 ("", "id => aprop", Delimfix "_"), |
156 ("", "var => aprop", Delimfix "_"), |
157 ("", "var => aprop", Delimfix "_"), |
157 ("_aprop", "aprop => prop", Delimfix "PROP _"), |
158 ("_aprop", "aprop => prop", Delimfix "PROP _"), |
158 ("", "prop => asms", Delimfix "_"), |
159 ("", "prop => asms", Delimfix "_"), |
159 ("_asms", "[prop, asms] => asms", Delimfix "_;/ _"), |
160 ("_asms", "[prop, asms] => asms", Delimfix "_;/ _"), |