changeset 32960 | 69916a850301 |
parent 19769 | c40ce2de2020 |
32959:23a8c5ac35f8 | 32960:69916a850301 |
---|---|
1 (* ID: $Id$ |
1 (* |
2 Author: Sava Krsti\'{c} and John Matthews |
2 Author: Sava Krsti\'{c} and John Matthews |
3 *) |
3 *) |
4 |
4 |
5 header {* Example use if an inductive invariant to solve termination conditions *} |
5 header {* Example use if an inductive invariant to solve termination conditions *} |
6 |
6 |
7 theory InductiveInvariant_examples imports InductiveInvariant begin |
7 theory InductiveInvariant_examples imports InductiveInvariant begin |