| changeset 32960 | 69916a850301 |
| parent 21404 | eb85850d3eb7 |
| child 44013 | 5cfc1c36ae97 |
--- a/src/HOL/ex/InductiveInvariant.thy Sat Oct 17 01:05:59 2009 +0200 +++ b/src/HOL/ex/InductiveInvariant.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 {* Some of the results in Inductive Invariants for Nested Recursion *}