equal
deleted
inserted
replaced
440 inductive predicate by stating some introduction rules and then the packages |
440 inductive predicate by stating some introduction rules and then the packages |
441 makes the equivalent definition and derives from it the needed properties. |
441 makes the equivalent definition and derives from it the needed properties. |
442 *} |
442 *} |
443 |
443 |
444 text {* |
444 text {* |
445 From a high-level perspective the package consists of 6 subtasks: |
445 (FIXME: perhaps move somewhere else) |
446 |
446 |
447 |
447 The point of these examples is to get a feeling what the automatic proofs |
448 |
448 should do in order to solve all inductive definitions we throw at them. For this |
|
449 it is instructive to look at the general construction principle |
|
450 of inductive definitions, which we shall do in the next section. |
449 *} |
451 *} |
450 |
452 |
451 |
453 |
452 (*<*) |
454 (*<*) |
453 end |
455 end |