| changeset 16417 | 9bc16273c2d4 |
| parent 15270 | 8b3f707a78a7 |
| child 19593 | c52a4360a41d |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
1 (*<*) |
1 (*<*) |
2 theory termination = examples: |
2 theory termination imports examples begin |
3 (*>*) |
3 (*>*) |
4 |
4 |
5 text{* |
5 text{* |
6 When a function~$f$ is defined via \isacommand{recdef}, Isabelle tries to prove |
6 When a function~$f$ is defined via \isacommand{recdef}, Isabelle tries to prove |
7 its termination with the help of the user-supplied measure. Each of the examples |
7 its termination with the help of the user-supplied measure. Each of the examples |