243 invocation is called @{ML add_inductive_i in SimpleInductivePackage}. Both |
243 invocation is called @{ML add_inductive_i in SimpleInductivePackage}. Both |
244 of these functions take as arguments the names and types of the inductive |
244 of these functions take as arguments the names and types of the inductive |
245 predicates, the names and types of their parameters, the actual introduction |
245 predicates, the names and types of their parameters, the actual introduction |
246 rules and a \emph{local theory}. They return a local theory containing the |
246 rules and a \emph{local theory}. They return a local theory containing the |
247 definition and the induction principle as well introduction rules. |
247 definition and the induction principle as well introduction rules. |
248 |
|
249 In contrast to an ordinary theory, which simply consists of a type |
|
250 signature, as well as tables for constants, axioms and theorems, a local |
|
251 theory also contains additional context information, such as locally fixed |
|
252 variables and local assumptions that may be used by the package. The type |
|
253 @{ML_type local_theory} is identical to the type of \emph{proof contexts} |
|
254 @{ML_type "Proof.context"}, although not every proof context constitutes a |
|
255 valid local theory. |
|
256 |
|
257 |
248 |
258 Note that @{ML add_inductive_i in SimpleInductivePackage} expects |
249 Note that @{ML add_inductive_i in SimpleInductivePackage} expects |
259 the types of the predicates and parameters to be specified using the |
250 the types of the predicates and parameters to be specified using the |
260 datatype @{ML_type typ} of Isabelle's logical framework, whereas @{ML |
251 datatype @{ML_type typ} of Isabelle's logical framework, whereas @{ML |
261 add_inductive in SimpleInductivePackage} expects them to be given as |
252 add_inductive in SimpleInductivePackage} expects them to be given as |