# HG changeset patch
# User haftmann
# Date 1232552851 -3600
# Node ID 117b88da143c8a61310e0d1018ed6254be4e4fb4
# Parent  cb520b766e0086fb5679ffd2489c45d1b219ccf0
dropped ID

diff -r cb520b766e00 -r 117b88da143c src/HOL/ATP_Linkup.thy
--- a/src/HOL/ATP_Linkup.thy	Wed Jan 21 16:47:04 2009 +0100
+++ b/src/HOL/ATP_Linkup.thy	Wed Jan 21 16:47:31 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/ATP_Linkup.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson
     Author:     Jia Meng, NICTA
     Author:     Fabian Immler, TUM
diff -r cb520b766e00 -r 117b88da143c src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Wed Jan 21 16:47:04 2009 +0100
+++ b/src/HOL/Datatype.thy	Wed Jan 21 16:47:31 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Datatype.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
 
diff -r cb520b766e00 -r 117b88da143c src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Jan 21 16:47:04 2009 +0100
+++ b/src/HOL/Finite_Set.thy	Wed Jan 21 16:47:31 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Finite_Set.thy
-    ID:         $Id$
     Author:     Tobias Nipkow, Lawrence C Paulson and Markus Wenzel
                 with contributions by Jeremy Avigad
 *)
diff -r cb520b766e00 -r 117b88da143c src/HOL/FunDef.thy
--- a/src/HOL/FunDef.thy	Wed Jan 21 16:47:04 2009 +0100
+++ b/src/HOL/FunDef.thy	Wed Jan 21 16:47:31 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/FunDef.thy
-    ID:         $Id$
     Author:     Alexander Krauss, TU Muenchen
 *)
 
diff -r cb520b766e00 -r 117b88da143c src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Wed Jan 21 16:47:04 2009 +0100
+++ b/src/HOL/Lattices.thy	Wed Jan 21 16:47:31 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Lattices.thy
-    ID:         $Id$
     Author:     Tobias Nipkow
 *)
 
diff -r cb520b766e00 -r 117b88da143c src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Wed Jan 21 16:47:04 2009 +0100
+++ b/src/HOL/Orderings.thy	Wed Jan 21 16:47:31 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Orderings.thy
-    ID:         $Id$
     Author:     Tobias Nipkow, Markus Wenzel, and Larry Paulson
 *)
 
diff -r cb520b766e00 -r 117b88da143c src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Wed Jan 21 16:47:04 2009 +0100
+++ b/src/HOL/Wellfounded.thy	Wed Jan 21 16:47:31 2009 +0100
@@ -1,5 +1,4 @@
-(*  ID:         $Id$
-    Author:     Tobias Nipkow
+(*  Author:     Tobias Nipkow
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Author:     Konrad Slind, Alexander Krauss
     Copyright   1992-2008  University of Cambridge and TU Muenchen
diff -r cb520b766e00 -r 117b88da143c src/Pure/primitive_defs.ML
--- a/src/Pure/primitive_defs.ML	Wed Jan 21 16:47:04 2009 +0100
+++ b/src/Pure/primitive_defs.ML	Wed Jan 21 16:47:31 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      Pure/primitive_defs.ML
-    ID:         $Id$
     Author:     Makarius
 
 Primitive definition forms.
diff -r cb520b766e00 -r 117b88da143c src/ZF/Inductive_ZF.thy
--- a/src/ZF/Inductive_ZF.thy	Wed Jan 21 16:47:04 2009 +0100
+++ b/src/ZF/Inductive_ZF.thy	Wed Jan 21 16:47:31 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      ZF/Inductive_ZF.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
diff -r cb520b766e00 -r 117b88da143c src/ZF/Main_ZF.thy
--- a/src/ZF/Main_ZF.thy	Wed Jan 21 16:47:04 2009 +0100
+++ b/src/ZF/Main_ZF.thy	Wed Jan 21 16:47:31 2009 +0100
@@ -1,5 +1,3 @@
-(*$Id$*)
-
 header{*Theory Main: Everything Except AC*}
 
 theory Main_ZF imports List_ZF IntDiv_ZF CardinalArith begin