equal
deleted
inserted
replaced
218 end; |
218 end; |
219 (* @end *) |
219 (* @end *) |
220 |
220 |
221 (* @chunk parser *) |
221 (* @chunk parser *) |
222 val spec_parser = |
222 val spec_parser = |
223 OuterParse.opt_target -- |
223 Parse.opt_target -- |
224 OuterParse.fixes -- |
224 Parse.fixes -- |
225 OuterParse.for_fixes -- |
225 Parse.for_fixes -- |
226 Scan.optional |
226 Scan.optional |
227 (OuterParse.$$$ "where" |-- |
227 (Parse.$$$ "where" |-- |
228 OuterParse.!!! |
228 Parse.!!! |
229 (OuterParse.enum1 "|" |
229 (Parse.enum1 "|" |
230 (SpecParse.opt_thm_name ":" -- OuterParse.prop))) [] |
230 (Parse_Spec.opt_thm_name ":" -- Parse.prop))) [] |
231 (* @end *) |
231 (* @end *) |
232 |
232 |
233 (* @chunk syntax *) |
233 (* @chunk syntax *) |
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 _ = OuterSyntax.command "simple_inductive" "define inductive predicates" |
239 val _ = Outer_Syntax.command "simple_inductive" "define inductive predicates" |
240 OuterKeyword.thy_decl specification |
240 Keyword.thy_decl specification |
241 (* @end *) |
241 (* @end *) |
242 |
242 |
243 end; |
243 end; |