src/HOL/ex/InductiveInvariant_examples.thy
changeset 32960 69916a850301
parent 19769 c40ce2de2020
--- a/src/HOL/ex/InductiveInvariant_examples.thy	Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/ex/InductiveInvariant_examples.thy	Sat Oct 17 14:43:18 2009 +0200
@@ -1,5 +1,5 @@
-(*  ID:         $Id$
-    Author:	Sava Krsti\'{c} and John Matthews
+(*
+    Author:     Sava Krsti\'{c} and John Matthews
 *)
 
 header {* Example use if an inductive invariant to solve termination conditions *}