equal
deleted
inserted
replaced
136 val _ = OuterSyntax.local_theory "simple_inductive2" |
136 val _ = OuterSyntax.local_theory "simple_inductive2" |
137 "definition of simple inductive predicates" |
137 "definition of simple inductive predicates" |
138 OuterKeyword.thy_decl specification*} |
138 OuterKeyword.thy_decl specification*} |
139 |
139 |
140 text {* |
140 text {* |
141 We call @{ML [index] local_theory in OuterSyntax} with the kind-indicator |
141 We call @{ML_ind [index] local_theory in OuterSyntax} with the kind-indicator |
142 @{ML [index] thy_decl in OuterKeyword} since the package does not need to open |
142 @{ML_ind [index] thy_decl in OuterKeyword} 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 |
149 ``naked'' strings: they have no type yet (even if we annotate them with |
149 ``naked'' strings: they have no type yet (even if we annotate them with |
150 types) and they are also not defined constants yet (which the predicates |
150 types) and they are also not defined constants yet (which the predicates |
151 eventually will be). Also the introduction rules are just strings. What we have |
151 eventually will be). Also the introduction rules are just strings. What we have |
152 to do first is to transform the parser's output into some internal |
152 to do first is to transform the parser's output into some internal |
153 datastructures that can be processed further. For this we can use the |
153 datastructures that can be processed further. For this we can use the |
154 function @{ML [index] read_spec in Specification}. This function takes some strings |
154 function @{ML_ind [index] read_spec in Specification}. This function takes some strings |
155 (with possible typing annotations) and some rule specifications, and attempts |
155 (with possible typing annotations) and some rule specifications, and attempts |
156 to find a typing according to the given type constraints given by the |
156 to find a typing according to the given type constraints given by the |
157 user and the type constraints by the ``ambient'' theory. It returns |
157 user and the type constraints by the ``ambient'' theory. It returns |
158 the type for the predicates and also returns typed terms for the |
158 the type for the predicates and also returns typed terms for the |
159 introduction rules. So at the heart of the function |
159 introduction rules. So at the heart of the function |