changeset 16417 | 9bc16273c2d4 |
parent 11458 | 09a6c44a48ea |
16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
---|---|
1 (*<*) |
1 (*<*) |
2 theory Induction = examples + simplification:; |
2 theory Induction imports examples simplification begin; |
3 (*>*) |
3 (*>*) |
4 |
4 |
5 text{* |
5 text{* |
6 Assuming we have defined our function such that Isabelle could prove |
6 Assuming we have defined our function such that Isabelle could prove |
7 termination and that the recursion equations (or some suitable derived |
7 termination and that the recursion equations (or some suitable derived |