equal
deleted
inserted
replaced
132 fun add_inductive pred_specs rule_specs lthy = lthy*}(*>*) |
132 fun add_inductive pred_specs rule_specs lthy = lthy*}(*>*) |
133 ML_val %linenosgray{*val specification : (local_theory -> local_theory) parser = |
133 ML_val %linenosgray{*val specification : (local_theory -> local_theory) parser = |
134 spec_parser >> |
134 spec_parser >> |
135 (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs) |
135 (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs) |
136 |
136 |
137 val _ = Outer_Syntax.local_theory ("simple_inductive2", Keyword.thy_decl) |
137 val _ = Outer_Syntax.local_theory @{command_spec "simple_inductive2"} |
138 "definition of simple inductive predicates" |
138 "definition of simple inductive predicates" |
139 specification*} |
139 specification*} |
140 |
140 |
141 text {* |
141 text {* |
142 We call @{ML_ind local_theory in Outer_Syntax} with the kind-indicator |
142 We call @{ML_ind local_theory in Outer_Syntax} with the kind-indicator |