149 ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"} |
149 ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"} |
150 |
150 |
151 then we get back the specifications of the predicates (with type and syntax annotations), |
151 then we get back the specifications of the predicates (with type and syntax annotations), |
152 and specifications of the introduction rules. This is all the information we |
152 and specifications of the introduction rules. This is all the information we |
153 need for calling the package and setting up the keyword. The latter is |
153 need for calling the package and setting up the keyword. The latter is |
154 done in Lines 5 to 7 in the code below. |
154 done in Lines 5 to 7 in the code below.\footnote{FIXME: Is there a way to state |
155 *} |
155 here @{text "simple_inductive"}?} |
156 |
156 *} |
157 (*<*) |
157 (*<*)ML %no{*fun add_inductive_cmd pred_specs rule_specs lthy = lthy |
158 ML %linenos |
158 fun add_inductive pred_specs rule_specs lthy = lthy*}(*>*) |
159 {* fun add_inductive_cmd pred_specs rule_specs lthy = lthy |
|
160 fun add_inductive pred_specs rule_specs lthy = lthy *} |
|
161 (*>*) |
|
162 |
|
163 ML_val %linenosgray{*val specification = |
159 ML_val %linenosgray{*val specification = |
164 spec_parser >> |
160 spec_parser >> |
165 (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs) |
161 (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs) |
166 |
162 |
167 val _ = OuterSyntax.local_theory "simple_inductive2" |
163 val _ = OuterSyntax.local_theory "simple_inductive2" |