--- a/src/HOL/ex/InductiveInvariant_examples.thy Wed Sep 14 22:04:38 2005 +0200
+++ b/src/HOL/ex/InductiveInvariant_examples.thy Wed Sep 14 22:08:08 2005 +0200
@@ -1,7 +1,10 @@
-theory InductiveInvariant_examples imports InductiveInvariant begin
+(* ID: $Id$
+ Author: Sava Krsti\'{c} and John Matthews
+*)
-(** Authors: Sava Krsti\'{c} and John Matthews **)
-(** Date: Oct 17, 2003 **)
+header {* Example use if an inductive invariant to solve termination conditions *}
+
+theory InductiveInvariant_examples imports InductiveInvariant begin
text "A simple example showing how to use an inductive invariant
to solve termination conditions generated by recdef on
@@ -124,4 +127,4 @@
by (subst ninety_one.simps,
simp add: ninety_one_tc measure_def inv_image_def)
-end
\ No newline at end of file
+end