equal
deleted
inserted
replaced
163 val _ = OuterSyntax.local_theory "simple_inductive2" |
163 val _ = OuterSyntax.local_theory "simple_inductive2" |
164 "definition of simple inductive predicates" |
164 "definition of simple inductive predicates" |
165 OuterKeyword.thy_decl specification*} |
165 OuterKeyword.thy_decl specification*} |
166 |
166 |
167 text {* |
167 text {* |
168 We call @{ML local_theory in OuterSyntax} with the kind-indicator |
168 We call @{ML [index] local_theory in OuterSyntax} with the kind-indicator |
169 @{ML thy_decl in OuterKeyword} since the package does not need to open |
169 @{ML [index] thy_decl in OuterKeyword} since the package does not need to open |
170 up any proof (see Section~\ref{sec:newcommand}). |
170 up any proof (see Section~\ref{sec:newcommand}). |
171 The auxiliary function @{text specification} in Lines 1 to 3 |
171 The auxiliary function @{text specification} in Lines 1 to 3 |
172 gathers the information from the parser to be processed further |
172 gathers the information from the parser to be processed further |
173 by the function @{text "add_inductive_cmd"}, which we describe below. |
173 by the function @{text "add_inductive_cmd"}, which we describe below. |
174 |
174 |
176 ``naked'' strings: they have no type yet (even if we annotate them with |
176 ``naked'' strings: they have no type yet (even if we annotate them with |
177 types) and they are also not defined constants yet (which the predicates |
177 types) and they are also not defined constants yet (which the predicates |
178 eventually will be). Also the introduction rules are just strings. What we have |
178 eventually will be). Also the introduction rules are just strings. What we have |
179 to do first is to transform the parser's output into some internal |
179 to do first is to transform the parser's output into some internal |
180 datastructures that can be processed further. For this we can use the |
180 datastructures that can be processed further. For this we can use the |
181 function @{ML read_spec in Specification}. This function takes some strings |
181 function @{ML [index] read_spec in Specification}. This function takes some strings |
182 (with possible typing annotations) and some rule specifications, and attempts |
182 (with possible typing annotations) and some rule specifications, and attempts |
183 to find a typing according to the given type constraints given by the |
183 to find a typing according to the given type constraints given by the |
184 user and the type constraints by the ``ambient'' theory. It returns |
184 user and the type constraints by the ``ambient'' theory. It returns |
185 the type for the predicates and also returns typed terms for the |
185 the type for the predicates and also returns typed terms for the |
186 introduction rules. So at the heart of the function |
186 introduction rules. So at the heart of the function |