equal
deleted
inserted
replaced
19 struct |
19 struct |
20 |
20 |
21 (* @chunk make_definitions *) |
21 (* @chunk make_definitions *) |
22 fun make_defs ((binding, syn), trm) lthy = |
22 fun make_defs ((binding, syn), trm) lthy = |
23 let |
23 let |
24 val arg = ((binding, syn), (Attrib.empty_binding, trm)) |
24 val arg = ((binding, syn), ((Binding.suffix_name "_def" binding, []), trm)) |
25 val ((_, (_ , thm)), lthy) = Local_Theory.define arg lthy |
25 val ((_, (_ , thm)), lthy) = Local_Theory.define arg lthy |
26 in |
26 in |
27 (thm, lthy) |
27 (thm, lthy) |
28 end |
28 end |
29 (* @end *) |
29 (* @end *) |
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" "define inductive predicates" |
239 val _ = Outer_Syntax.command ("simple_inductive", Keyword.thy_decl) "define inductive predicates" |
240 Keyword.thy_decl specification |
240 specification |
241 (* @end *) |
241 (* @end *) |
242 |
242 |
243 end; |
243 end; |