1.1 --- a/src/HOL/ATP_Linkup.thy	Wed Jan 21 16:47:04 2009 +0100
     1.2 +++ b/src/HOL/ATP_Linkup.thy	Wed Jan 21 16:47:31 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/ATP_Linkup.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Lawrence C Paulson
     1.7      Author:     Jia Meng, NICTA
     1.8      Author:     Fabian Immler, TUM

     2.1 --- a/src/HOL/Datatype.thy	Wed Jan 21 16:47:04 2009 +0100
     2.2 +++ b/src/HOL/Datatype.thy	Wed Jan 21 16:47:31 2009 +0100
     2.3 @@ -1,5 +1,4 @@
     2.4  (*  Title:      HOL/Datatype.thy
     2.5 -    ID:         $Id$
     2.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7      Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
     2.8  

     3.1 --- a/src/HOL/Finite_Set.thy	Wed Jan 21 16:47:04 2009 +0100
     3.2 +++ b/src/HOL/Finite_Set.thy	Wed Jan 21 16:47:31 2009 +0100
     3.3 @@ -1,5 +1,4 @@
     3.4  (*  Title:      HOL/Finite_Set.thy
     3.5 -    ID:         $Id$
     3.6      Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
     3.7                  with contributions by Jeremy Avigad
     3.8  *)

     4.1 --- a/src/HOL/FunDef.thy	Wed Jan 21 16:47:04 2009 +0100
     4.2 +++ b/src/HOL/FunDef.thy	Wed Jan 21 16:47:31 2009 +0100
     4.3 @@ -1,5 +1,4 @@
     4.4  (*  Title:      HOL/FunDef.thy
     4.5 -    ID:         $Id$
     4.6      Author:     Alexander Krauss, TU Muenchen
     4.7  *)
     4.8  

     5.1 --- a/src/HOL/Lattices.thy	Wed Jan 21 16:47:04 2009 +0100
     5.2 +++ b/src/HOL/Lattices.thy	Wed Jan 21 16:47:31 2009 +0100
     5.3 @@ -1,5 +1,4 @@
     5.4  (*  Title:      HOL/Lattices.thy
     5.5 -    ID:         $Id$
     5.6      Author:     Tobias Nipkow
     5.7  *)
     5.8  

     6.1 --- a/src/HOL/Orderings.thy	Wed Jan 21 16:47:04 2009 +0100
     6.2 +++ b/src/HOL/Orderings.thy	Wed Jan 21 16:47:31 2009 +0100
     6.3 @@ -1,5 +1,4 @@
     6.4  (*  Title:      HOL/Orderings.thy
     6.5 -    ID:         $Id$
     6.6      Author:     Tobias Nipkow, Markus Wenzel, and Larry Paulson
     6.7  *)
     6.8  

     7.1 --- a/src/HOL/Wellfounded.thy	Wed Jan 21 16:47:04 2009 +0100
     7.2 +++ b/src/HOL/Wellfounded.thy	Wed Jan 21 16:47:31 2009 +0100
     7.3 @@ -1,5 +1,4 @@
     7.4 -(*  ID:         $Id$
     7.5 -    Author:     Tobias Nipkow
     7.6 +(*  Author:     Tobias Nipkow
     7.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.8      Author:     Konrad Slind, Alexander Krauss
     7.9      Copyright   1992-2008  University of Cambridge and TU Muenchen

     8.1 --- a/src/Pure/primitive_defs.ML	Wed Jan 21 16:47:04 2009 +0100
     8.2 +++ b/src/Pure/primitive_defs.ML	Wed Jan 21 16:47:31 2009 +0100
     8.3 @@ -1,5 +1,4 @@
     8.4  (*  Title:      Pure/primitive_defs.ML
     8.5 -    ID:         $Id$
     8.6      Author:     Makarius
     8.7  
     8.8  Primitive definition forms.

     9.1 --- a/src/ZF/Inductive_ZF.thy	Wed Jan 21 16:47:04 2009 +0100
     9.2 +++ b/src/ZF/Inductive_ZF.thy	Wed Jan 21 16:47:31 2009 +0100
     9.3 @@ -1,5 +1,4 @@
     9.4  (*  Title:      ZF/Inductive_ZF.thy
     9.5 -    ID:         $Id$
     9.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.7      Copyright   1993  University of Cambridge
     9.8  

    10.1 --- a/src/ZF/Main_ZF.thy	Wed Jan 21 16:47:04 2009 +0100
    10.2 +++ b/src/ZF/Main_ZF.thy	Wed Jan 21 16:47:31 2009 +0100
    10.3 @@ -1,5 +1,3 @@
    10.4 -(*$Id$*)
    10.5 -
    10.6  header{*Theory Main: Everything Except AC*}
    10.7  
    10.8  theory Main_ZF imports List_ZF IntDiv_ZF CardinalArith begin