changeset 32960 | 69916a850301 |
parent 21404 | eb85850d3eb7 |
child 44013 | 5cfc1c36ae97 |
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 {* Some of the results in Inductive Invariants for Nested Recursion *} |
5 header {* Some of the results in Inductive Invariants for Nested Recursion *} |
6 |
6 |
7 theory InductiveInvariant imports Main begin |
7 theory InductiveInvariant imports Main begin |