equal
deleted
inserted
replaced
234 val specification = |
234 val specification = |
235 spec_parser >> |
235 spec_parser >> |
236 (fn (((loc, preds), params), specs) => |
236 (fn (((loc, preds), params), specs) => |
237 Toplevel.local_theory loc (add_inductive preds params specs)) |
237 Toplevel.local_theory loc (add_inductive preds params specs)) |
238 |
238 |
239 val _ = Outer_Syntax.command ("simple_inductive", Keyword.thy_decl) "define inductive predicates" |
239 val _ = Outer_Syntax.command @{command_spec "simple_inductive"} "define inductive predicates" |
240 specification |
240 specification |
241 (* @end *) |
241 (* @end *) |
242 |
242 |
243 end; |
243 end; |