equal
deleted
inserted
replaced
127 need for calling the package and setting up the keyword. The latter is |
127 need for calling the package and setting up the keyword. The latter is |
128 done in Lines 5 to 7 in the code below. |
128 done in Lines 5 to 7 in the code below. |
129 *} |
129 *} |
130 (*<*)ML %no{*fun add_inductive_cmd pred_specs rule_specs lthy = lthy |
130 (*<*)ML %no{*fun add_inductive_cmd pred_specs rule_specs lthy = lthy |
131 fun add_inductive pred_specs rule_specs lthy = lthy*}(*>*) |
131 fun add_inductive pred_specs rule_specs lthy = lthy*}(*>*) |
132 ML_val %linenosgray{*val specification = |
132 ML_val %linenosgray{*val specification : (local_theory -> local_theory) parser = |
133 spec_parser >> |
133 spec_parser >> |
134 (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs) |
134 (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs) |
135 |
135 |
136 val _ = OuterSyntax.local_theory "simple_inductive2" |
136 val _ = OuterSyntax.local_theory "simple_inductive2" |
137 "definition of simple inductive predicates" |
137 "definition of simple inductive predicates" |