src/HOL/ex/InductiveInvariant_examples.thy
changeset 17388 495c799df31d
parent 16417 9bc16273c2d4
child 19623 12e6cc4382ae
     1.1 --- a/src/HOL/ex/InductiveInvariant_examples.thy	Wed Sep 14 22:04:38 2005 +0200
     1.2 +++ b/src/HOL/ex/InductiveInvariant_examples.thy	Wed Sep 14 22:08:08 2005 +0200
     1.3 @@ -1,7 +1,10 @@
     1.4 -theory InductiveInvariant_examples imports InductiveInvariant  begin
     1.5 +(*  ID:         $Id$
     1.6 +    Author:	Sava Krsti\'{c} and John Matthews
     1.7 +*)
     1.8  
     1.9 -(** Authors: Sava Krsti\'{c} and John Matthews **)
    1.10 -(**    Date: Oct 17, 2003                      **)
    1.11 +header {* Example use if an inductive invariant to solve termination conditions *}
    1.12 +
    1.13 +theory InductiveInvariant_examples imports InductiveInvariant  begin
    1.14  
    1.15  text "A simple example showing how to use an inductive invariant
    1.16        to solve termination conditions generated by recdef on
    1.17 @@ -124,4 +127,4 @@
    1.18  by (subst ninety_one.simps,
    1.19      simp add: ninety_one_tc measure_def inv_image_def)
    1.20  
    1.21 -end
    1.22 \ No newline at end of file
    1.23 +end