equal
deleted
inserted
replaced
189 (OuterParse.enum1 "|" |
189 (OuterParse.enum1 "|" |
190 (SpecParse.opt_thm_name ":" -- OuterParse.prop))) [] |
190 (SpecParse.opt_thm_name ":" -- OuterParse.prop))) [] |
191 (* @end *) |
191 (* @end *) |
192 |
192 |
193 (* @chunk syntax *) |
193 (* @chunk syntax *) |
194 val ind_decl = |
194 val specification = |
195 spec_parser >> |
195 spec_parser >> |
196 (fn (((loc, preds), params), specs) => |
196 (fn (((loc, preds), params), specs) => |
197 Toplevel.local_theory loc (add_inductive preds params specs)) |
197 Toplevel.local_theory loc (add_inductive preds params specs)) |
198 |
198 |
199 val _ = OuterSyntax.command "simple_inductive" "define inductive predicates" |
199 val _ = OuterSyntax.command "simple_inductive" "define inductive predicates" |
200 OuterKeyword.thy_decl ind_decl |
200 OuterKeyword.thy_decl specification |
201 (* @end *) |
201 (* @end *) |
202 |
202 |
203 end; |
203 end; |