Plain, Main form meeting points in import hierarchy

--- a/src/HOL/Dense_Linear_Order.thy	Wed Jan 28 11:03:16 2009 +0100
+++ b/src/HOL/Dense_Linear_Order.thy	Wed Jan 28 11:03:42 2009 +0100
@@ -1,10 +1,12 @@
-(* Author: Amine Chaieb, TU Muenchen *)
+(*  Title       : HOL/Dense_Linear_Order.thy
+    Author      : Amine Chaieb, TU Muenchen
+*)
 
 header {* Dense linear order without endpoints
   and a quantifier elimination procedure in Ferrante and Rackoff style *}
 
 theory Dense_Linear_Order
-imports Plain Groebner_Basis
+imports Plain Groebner_Basis Main
 uses
   "~~/src/HOL/Tools/Qelim/langford_data.ML"
   "~~/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML"

--- a/src/HOL/Equiv_Relations.thy	Wed Jan 28 11:03:16 2009 +0100
+++ b/src/HOL/Equiv_Relations.thy	Wed Jan 28 11:03:42 2009 +0100
@@ -1,12 +1,11 @@
-(*  ID:         $Id$
-    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
+(*  Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1996  University of Cambridge
 *)
 
 header {* Equivalence Relations in Higher-Order Set Theory *}
 
 theory Equiv_Relations
-imports Finite_Set Relation
+imports Finite_Set Relation Plain
 begin
 
 subsection {* Equivalence relations *}

--- a/src/HOL/GCD.thy	Wed Jan 28 11:03:16 2009 +0100
+++ b/src/HOL/GCD.thy	Wed Jan 28 11:03:42 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/GCD.thy
-    ID:         $Id$
     Author:     Christophe Tabacznyj and Lawrence C Paulson
     Copyright   1996  University of Cambridge
 *)
@@ -7,7 +6,7 @@
 header {* The Greatest Common Divisor *}
 
 theory GCD
-imports Plain Presburger
+imports Plain Presburger Main
 begin
 
 text {*

--- a/src/HOL/Hilbert_Choice.thy	Wed Jan 28 11:03:16 2009 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Wed Jan 28 11:03:42 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Hilbert_Choice.thy
-    ID:         $Id$
     Author:     Lawrence C Paulson
     Copyright   2001  University of Cambridge
 *)
@@ -7,7 +6,7 @@
 header {* Hilbert's Epsilon-Operator and the Axiom of Choice *}
 
 theory Hilbert_Choice
-imports Nat Wellfounded
+imports Nat Wellfounded Plain
 uses ("Tools/meson.ML") ("Tools/specification_package.ML")
 begin