156 \begin{matharray}{rcl} 
156 \begin{matharray}{rcl} 
157 induct & : & \isarmeth \\ 
157 induct & : & \isarmeth \\ 
158 \end{matharray} 
158 \end{matharray} 
159 
159 
160 The $induct$ method provides a uniform interface to induction over datatypes, 
160 The $induct$ method provides a uniform interface to induction over datatypes, 
161 inductive sets, and recursive functions. Basically, it is just an interface 
161 inductive sets, recursive functions etc. Basically, it is just an interface 
162 to the $rule$ method applied to appropriate instances of the corresponding 
162 to the $rule$ method applied to appropriate instances of the corresponding 
163 induction rules. 
163 induction rules. 
164 
164 
165 \begin{rail} 
165 \begin{rail} 
166 'induct' (inst * 'and') kind? 
166 'induct' (inst * 'and') kind? 
167 ; 
167 ; 
168 
168 
169 inst: term term? 
169 inst: term term? 
170 ; 
170 ; 
171 kind: ('type'  'set'  'function') ':' nameref 
171 kind: ('type'  'set'  'function'  'rule') ':' nameref 
172 ; 
172 ; 
173 \end{rail} 
173 \end{rail} 
174 
174 
175 \begin{descr} 
175 \begin{descr} 
176 \item [$induct~insts~kind$] abbreviates method $rule~R$, where $R$ is the 
176 \item [$induct~insts~kind$] abbreviates method $rule~R$, where $R$ is the 
177 induction rule of the type~/ set~/ function specified by $kind$ and 
177 induction rule specified by $kind$ and instantiated by $insts$. The rule is 
178 instantiated by $insts$. The latter either consists of pairs $P$ $x$ 
178 either that of some type, set, or recursive function (defined via TFL), or 
179 (induction predicate and variable), where $P$ is optional. If $kind$ is 
179 given explicitly. 

180 

181 The instantiation basically consists of a list of $P$ $x$ (induction 

182 predicate and variable) specifications, where $P$ is optional. If $kind$ is 
180 omitted, the default is to pick a datatype induction rule according to the 
183 omitted, the default is to pick a datatype induction rule according to the 
181 type of some induction variable, which may not be omitted that case. 
184 type of some induction variable, which may not be omitted that case. 
182 \end{descr} 
185 \end{descr} 
183 
186 
184 
187 