equal
deleted
inserted
replaced
177 induction proceeds. |
177 induction proceeds. |
178 |
178 |
179 Write code that automates the derivation of the strong induction |
179 Write code that automates the derivation of the strong induction |
180 principles from the weak ones. |
180 principles from the weak ones. |
181 \end{exercise} |
181 \end{exercise} |
|
182 |
|
183 \begin{readmore} |
|
184 The standard inductive package is based on least fix-points. It allows more |
|
185 general introduction rules that can include any monotone operators and also |
|
186 provides a richer reasoning infrastructure. The code of this package can be found in |
|
187 @{ML_file "HOL/Tools/inductive_package.ML"}. |
|
188 \end{readmore} |
182 *} |
189 *} |
183 |
190 |
184 |
191 |
185 |
192 |
186 (*<*)end(*>*) |
193 (*<*)end(*>*) |