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 *}