equal
deleted
inserted
replaced
116 val parse_bnf_axiomatization = |
116 val parse_bnf_axiomatization = |
117 parse_bnf_axiomatization_options -- parse_type_args_named_constrained -- Parse.binding -- |
117 parse_bnf_axiomatization_options -- parse_type_args_named_constrained -- Parse.binding -- |
118 parse_witTs -- Parse.opt_mixfix -- parse_map_rel_bindings; |
118 parse_witTs -- Parse.opt_mixfix -- parse_map_rel_bindings; |
119 |
119 |
120 val _ = |
120 val _ = |
121 Outer_Syntax.local_theory @{command_spec "bnf_axiomatization"} "bnf declaration" |
121 Outer_Syntax.local_theory @{command_keyword bnf_axiomatization} "bnf declaration" |
122 (parse_bnf_axiomatization >> |
122 (parse_bnf_axiomatization >> |
123 (fn (((((plugins, bsTs), b), witTs), mx), (mapb, relb)) => |
123 (fn (((((plugins, bsTs), b), witTs), mx), (mapb, relb)) => |
124 bnf_axiomatization_cmd plugins bsTs b mx mapb relb witTs #> snd)); |
124 bnf_axiomatization_cmd plugins bsTs b mx mapb relb witTs #> snd)); |
125 |
125 |
126 end; |
126 end; |