explicit import of theory Main

--- a/src/HOL/Library/BigO.thy	Mon Dec 10 11:24:03 2007 +0100
+++ b/src/HOL/Library/BigO.thy	Mon Dec 10 11:24:06 2007 +0100
@@ -6,7 +6,7 @@
 header {* Big O notation *}
 
 theory BigO
-imports SetsAndFunctions
+imports Main SetsAndFunctions
 begin
 
 text {*

--- a/src/HOL/MetisExamples/BigO.thy	Mon Dec 10 11:24:03 2007 +0100
+++ b/src/HOL/MetisExamples/BigO.thy	Mon Dec 10 11:24:06 2007 +0100
@@ -8,7 +8,7 @@
 header {* Big O notation *}
 
 theory BigO
-imports SetsAndFunctions 
+imports Main SetsAndFunctions 
 begin
 
 subsection {* Definitions *}

--- a/src/HOL/MicroJava/BV/Semilat.thy	Mon Dec 10 11:24:03 2007 +0100
+++ b/src/HOL/MicroJava/BV/Semilat.thy	Mon Dec 10 11:24:06 2007 +0100
@@ -11,7 +11,9 @@
   \isaheader{Semilattices} 
 *}
 
-theory Semilat imports While_Combinator begin
+theory Semilat
+imports Main While_Combinator
+begin
 
 types 'a ord    = "'a \<Rightarrow> 'a \<Rightarrow> bool"
       'a binop  = "'a \<Rightarrow> 'a \<Rightarrow> 'a"

--- a/src/HOL/NumberTheory/Finite2.thy	Mon Dec 10 11:24:03 2007 +0100
+++ b/src/HOL/NumberTheory/Finite2.thy	Mon Dec 10 11:24:06 2007 +0100
@@ -6,7 +6,7 @@
 header {*Finite Sets and Finite Sums*}
 
 theory Finite2
-imports IntFact Infinite_Set
+imports Main IntFact Infinite_Set
 begin
 
 text{*

--- a/src/HOL/SET-Protocol/MessageSET.thy	Mon Dec 10 11:24:03 2007 +0100
+++ b/src/HOL/SET-Protocol/MessageSET.thy	Mon Dec 10 11:24:06 2007 +0100
@@ -5,7 +5,9 @@
 
 header{*The Message Theory, Modified for SET*}
 
-theory MessageSET imports NatPair begin
+theory MessageSET
+imports Main NatPair
+begin
 
 subsection{*General Lemmas*}
 

--- a/src/HOL/Unix/Unix.thy	Mon Dec 10 11:24:03 2007 +0100
+++ b/src/HOL/Unix/Unix.thy	Mon Dec 10 11:24:06 2007 +0100
@@ -6,7 +6,7 @@
 header {* Unix file-systems \label{sec:unix-file-system} *}
 
 theory Unix
-imports Nested_Environment List_Prefix
+imports Main Nested_Environment List_Prefix
 begin
 
 text {*

--- a/src/HOL/Word/Num_Lemmas.thy	Mon Dec 10 11:24:03 2007 +0100
+++ b/src/HOL/Word/Num_Lemmas.thy	Mon Dec 10 11:24:06 2007 +0100
@@ -5,7 +5,9 @@
 
 header {* Useful Numerical Lemmas *}
 
-theory Num_Lemmas imports Parity begin
+theory Num_Lemmas
+imports Main Parity
+begin
 
 lemma contentsI: "y = {x} ==> contents y = x" 
   unfolding contents_def by auto

--- a/src/HOL/ex/LocaleTest2.thy	Mon Dec 10 11:24:03 2007 +0100
+++ b/src/HOL/ex/LocaleTest2.thy	Mon Dec 10 11:24:06 2007 +0100
@@ -12,7 +12,7 @@
 header {* Test of Locale Interpretation *}
 
 theory LocaleTest2
-imports GCD
+imports Main GCD
 begin
 
 section {* Interpretation of Defined Concepts *}

--- a/src/HOL/ex/Reflected_Presburger.thy	Mon Dec 10 11:24:03 2007 +0100
+++ b/src/HOL/ex/Reflected_Presburger.thy	Mon Dec 10 11:24:06 2007 +0100
@@ -1,5 +1,5 @@
 theory Reflected_Presburger
-imports GCD Efficient_Nat
+imports Main GCD Efficient_Nat
 uses ("coopereif.ML") ("coopertac.ML")
 begin