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