| changeset 16417 | 9bc16273c2d4 |
| parent 15636 | 57c437b70521 |
| child 17388 | 495c799df31d |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
1 theory InductiveInvariant_examples = InductiveInvariant : |
1 theory InductiveInvariant_examples imports InductiveInvariant begin |
2 |
2 |
3 (** Authors: Sava Krsti\'{c} and John Matthews **) |
3 (** Authors: Sava Krsti\'{c} and John Matthews **) |
4 (** Date: Oct 17, 2003 **) |
4 (** Date: Oct 17, 2003 **) |
5 |
5 |
6 text "A simple example showing how to use an inductive invariant |
6 text "A simple example showing how to use an inductive invariant |