| changeset 16417 | 9bc16273c2d4 |
| parent 15636 | 57c437b70521 |
| child 17388 | 495c799df31d |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
1 theory InductiveInvariant = Main: |
1 theory InductiveInvariant imports Main begin |
2 |
2 |
3 (** Authors: Sava Krsti\'{c} and John Matthews **) |
3 (** Authors: Sava Krsti\'{c} and John Matthews **) |
4 (** Date: Sep 12, 2003 **) |
4 (** Date: Sep 12, 2003 **) |
5 |
5 |
6 text {* A formalization of some of the results in |
6 text {* A formalization of some of the results in |