| changeset 16417 | 9bc16273c2d4 |
| parent 15636 | 57c437b70521 |
| child 17388 | 495c799df31d |
--- a/src/HOL/ex/InductiveInvariant_examples.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/ex/InductiveInvariant_examples.thy Fri Jun 17 16:12:49 2005 +0200 @@ -1,4 +1,4 @@ -theory InductiveInvariant_examples = InductiveInvariant : +theory InductiveInvariant_examples imports InductiveInvariant begin (** Authors: Sava Krsti\'{c} and John Matthews **) (** Date: Oct 17, 2003 **)