59 less translates directly into the parser: |
59 less translates directly into the parser: |
60 |
60 |
61 *} |
61 *} |
62 |
62 |
63 ML{*val spec_parser = |
63 ML{*val spec_parser = |
64 OuterParse.fixes -- |
64 Parse.fixes -- |
65 Scan.optional |
65 Scan.optional |
66 (OuterParse.$$$ "where" |-- |
66 (Parse.$$$ "where" |-- |
67 OuterParse.!!! |
67 Parse.!!! |
68 (OuterParse.enum1 "|" |
68 (Parse.enum1 "|" |
69 (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*} |
69 (Parse_Spec.opt_thm_name ":" -- Parse.prop))) []*} |
70 |
70 |
71 text {* |
71 text {* |
72 which we explained in Section~\ref{sec:parsingspecs}. There is no code included |
72 which we explained in Section~\ref{sec:parsingspecs}. There is no code included |
73 for parsing the keyword and what is called a \emph{target}. The latter can be given |
73 for parsing the keyword and what is called a \emph{target}. The latter can be given |
74 optionally after the keyword. The target is an ``advanced'' feature which we will |
74 optionally after the keyword. The target is an ``advanced'' feature which we will |
93 simple_inductive (in rel) |
93 simple_inductive (in rel) |
94 accpart' |
94 accpart' |
95 where |
95 where |
96 accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x" |
96 accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x" |
97 (*<*)ML %no{*fun filtered_input str = |
97 (*<*)ML %no{*fun filtered_input str = |
98 filter OuterLex.is_proper (OuterSyntax.scan Position.none str) |
98 filter Token.is_proper (Outer_Syntax.scan Position.none str) |
99 fun parse p input = Scan.finite OuterLex.stopper (Scan.error p) input*}(*>*) |
99 fun parse p input = Scan.finite Token.stopper (Scan.error p) input*}(*>*) |
100 text {* |
100 text {* |
101 Note that in these definitions the parameter @{text R}, standing for the |
101 Note that in these definitions the parameter @{text R}, standing for the |
102 relation, is left implicit. For the moment we will ignore this kind |
102 relation, is left implicit. For the moment we will ignore this kind |
103 of implicit parameters and rely on the fact that the infrastructure will |
103 of implicit parameters and rely on the fact that the infrastructure will |
104 deal with them. Later, however, we will come back to them. |
104 deal with them. Later, however, we will come back to them. |
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 : (local_theory -> local_theory) parser = |
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 _ = Outer_Syntax.local_theory "simple_inductive2" |
137 "definition of simple inductive predicates" |
137 "definition of simple inductive predicates" |
138 OuterKeyword.thy_decl specification*} |
138 Keyword.thy_decl specification*} |
139 |
139 |
140 text {* |
140 text {* |
141 We call @{ML_ind local_theory in OuterSyntax} with the kind-indicator |
141 We call @{ML_ind local_theory in Outer_Syntax} with the kind-indicator |
142 @{ML_ind thy_decl in OuterKeyword} since the package does not need to open |
142 @{ML_ind thy_decl in Keyword} since the package does not need to open |
143 up any proof (see Section~\ref{sec:newcommand}). |
143 up any proof (see Section~\ref{sec:newcommand}). |
144 The auxiliary function @{text specification} in Lines 1 to 3 |
144 The auxiliary function @{text specification} in Lines 1 to 3 |
145 gathers the information from the parser to be processed further |
145 gathers the information from the parser to be processed further |
146 by the function @{text "add_inductive_cmd"}, which we describe below. |
146 by the function @{text "add_inductive_cmd"}, which we describe below. |
147 |
147 |