# HG changeset patch
# User haftmann
# Date 1238144711 -3600
# Node ID 0842e906300cd31055b2500162f2dd1c70deedc0
# Parent  9ffd27558916f5c16e067749e369e73a7209e631
normalized imports

diff -r 9ffd27558916 -r 0842e906300c src/HOL/Decision_Procs/Dense_Linear_Order.thy
--- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Fri Mar 27 10:05:08 2009 +0100
+++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Fri Mar 27 10:05:11 2009 +0100
@@ -6,7 +6,7 @@
   and a quantifier elimination procedure in Ferrante and Rackoff style *}
 
 theory Dense_Linear_Order
-imports Plain Groebner_Basis Main
+imports Main
 uses
   "~~/src/HOL/Tools/Qelim/langford_data.ML"
   "~~/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML"
diff -r 9ffd27558916 -r 0842e906300c src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Fri Mar 27 10:05:08 2009 +0100
+++ b/src/HOL/GCD.thy	Fri Mar 27 10:05:11 2009 +0100
@@ -6,7 +6,7 @@
 header {* The Greatest Common Divisor *}
 
 theory GCD
-imports Plain Presburger Main
+imports Main
 begin
 
 text {*
diff -r 9ffd27558916 -r 0842e906300c src/HOL/Imperative_HOL/Heap.thy
--- a/src/HOL/Imperative_HOL/Heap.thy	Fri Mar 27 10:05:08 2009 +0100
+++ b/src/HOL/Imperative_HOL/Heap.thy	Fri Mar 27 10:05:11 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      HOL/Library/Heap.thy
-    ID:         $Id$
     Author:     John Matthews, Galois Connections; Alexander Krauss, TU Muenchen
 *)
 
 header {* A polymorphic heap based on cantor encodings *}
 
 theory Heap
-imports Plain "~~/src/HOL/List" Countable Typerep
+imports Main Countable
 begin
 
 subsection {* Representable types *}
diff -r 9ffd27558916 -r 0842e906300c src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Fri Mar 27 10:05:08 2009 +0100
+++ b/src/HOL/Library/Permutation.thy	Fri Mar 27 10:05:11 2009 +0100
@@ -5,7 +5,7 @@
 header {* Permutations *}
 
 theory Permutation
-imports Plain Multiset
+imports Main Multiset
 begin
 
 inductive
diff -r 9ffd27558916 -r 0842e906300c src/HOL/Library/Pocklington.thy
--- a/src/HOL/Library/Pocklington.thy	Fri Mar 27 10:05:08 2009 +0100
+++ b/src/HOL/Library/Pocklington.thy	Fri Mar 27 10:05:11 2009 +0100
@@ -1,13 +1,11 @@
 (*  Title:      HOL/Library/Pocklington.thy
-    ID:         $Id$
     Author:     Amine Chaieb
 *)
 
 header {* Pocklington's Theorem for Primes *}
 
-
 theory Pocklington
-imports Plain "~~/src/HOL/List" "~~/src/HOL/Primes"
+imports Main Primes
 begin
 
 definition modeq:: "nat => nat => nat => bool"    ("(1[_ = _] '(mod _'))")
diff -r 9ffd27558916 -r 0842e906300c src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Fri Mar 27 10:05:08 2009 +0100
+++ b/src/HOL/Library/Polynomial.thy	Fri Mar 27 10:05:11 2009 +0100
@@ -6,7 +6,7 @@
 header {* Univariate Polynomials *}
 
 theory Polynomial
-imports Plain SetInterval Main
+imports Main
 begin
 
 subsection {* Definition of type @{text poly} *}
diff -r 9ffd27558916 -r 0842e906300c src/HOL/Library/Primes.thy
--- a/src/HOL/Library/Primes.thy	Fri Mar 27 10:05:08 2009 +0100
+++ b/src/HOL/Library/Primes.thy	Fri Mar 27 10:05:11 2009 +0100
@@ -6,7 +6,7 @@
 header {* Primality on nat *}
 
 theory Primes
-imports Plain "~~/src/HOL/ATP_Linkup" "~~/src/HOL/GCD" "~~/src/HOL/Parity"
+imports Complex_Main
 begin
 
 definition
diff -r 9ffd27558916 -r 0842e906300c src/HOL/Library/Product_ord.thy
--- a/src/HOL/Library/Product_ord.thy	Fri Mar 27 10:05:08 2009 +0100
+++ b/src/HOL/Library/Product_ord.thy	Fri Mar 27 10:05:11 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      HOL/Library/Product_ord.thy
-    ID:         $Id$
     Author:     Norbert Voelker
 *)
 
 header {* Order on product types *}
 
 theory Product_ord
-imports Plain
+imports Main
 begin
 
 instantiation "*" :: (ord, ord) ord
diff -r 9ffd27558916 -r 0842e906300c src/HOL/Library/Quicksort.thy
--- a/src/HOL/Library/Quicksort.thy	Fri Mar 27 10:05:08 2009 +0100
+++ b/src/HOL/Library/Quicksort.thy	Fri Mar 27 10:05:11 2009 +0100
@@ -1,12 +1,11 @@
-(*  ID:         $Id$
-    Author:     Tobias Nipkow
+(*  Author:     Tobias Nipkow
     Copyright   1994 TU Muenchen
 *)
 
 header{*Quicksort*}
 
 theory Quicksort
-imports Plain Multiset
+imports Main Multiset
 begin
 
 context linorder
diff -r 9ffd27558916 -r 0842e906300c src/HOL/Library/Quotient.thy
--- a/src/HOL/Library/Quotient.thy	Fri Mar 27 10:05:08 2009 +0100
+++ b/src/HOL/Library/Quotient.thy	Fri Mar 27 10:05:11 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      HOL/Library/Quotient.thy
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 *)
 
 header {* Quotient types *}
 
 theory Quotient
-imports Plain "~~/src/HOL/Hilbert_Choice"
+imports Main
 begin
 
 text {*
diff -r 9ffd27558916 -r 0842e906300c src/HOL/Library/RBT.thy
--- a/src/HOL/Library/RBT.thy	Fri Mar 27 10:05:08 2009 +0100
+++ b/src/HOL/Library/RBT.thy	Fri Mar 27 10:05:11 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      RBT.thy
-    ID:         $Id$
     Author:     Markus Reiter, TU Muenchen
     Author:     Alexander Krauss, TU Muenchen
 *)
@@ -8,7 +7,7 @@
 
 (*<*)
 theory RBT
-imports Plain AssocList
+imports Main AssocList
 begin
 
 datatype color = R | B
diff -r 9ffd27558916 -r 0842e906300c src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy	Fri Mar 27 10:05:08 2009 +0100
+++ b/src/HOL/Library/Ramsey.thy	Fri Mar 27 10:05:11 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      HOL/Library/Ramsey.thy
-    ID:         $Id$
     Author:     Tom Ridge. Converted to structured Isar by L C Paulson
 *)
 
 header "Ramsey's Theorem"
 
 theory Ramsey
-imports Plain "~~/src/HOL/Presburger" Infinite_Set
+imports Main Infinite_Set
 begin
 
 subsection {* Preliminaries *}
diff -r 9ffd27558916 -r 0842e906300c src/HOL/Library/SetsAndFunctions.thy
--- a/src/HOL/Library/SetsAndFunctions.thy	Fri Mar 27 10:05:08 2009 +0100
+++ b/src/HOL/Library/SetsAndFunctions.thy	Fri Mar 27 10:05:11 2009 +0100
@@ -5,7 +5,7 @@
 header {* Operations on sets and functions *}
 
 theory SetsAndFunctions
-imports Plain
+imports Main
 begin
 
 text {*
diff -r 9ffd27558916 -r 0842e906300c src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Fri Mar 27 10:05:08 2009 +0100
+++ b/src/HOL/Library/State_Monad.thy	Fri Mar 27 10:05:11 2009 +0100
@@ -5,7 +5,7 @@
 header {* Combinator syntax for generic, open state monads (single threaded monads) *}
 
 theory State_Monad
-imports Plain "~~/src/HOL/List"
+imports Main
 begin
 
 subsection {* Motivation *}
diff -r 9ffd27558916 -r 0842e906300c src/HOL/Library/Sublist_Order.thy
--- a/src/HOL/Library/Sublist_Order.thy	Fri Mar 27 10:05:08 2009 +0100
+++ b/src/HOL/Library/Sublist_Order.thy	Fri Mar 27 10:05:11 2009 +0100
@@ -1,13 +1,12 @@
 (*  Title:      HOL/Library/Sublist_Order.thy
-    ID:         $Id$
     Authors:    Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de>
-                Florian Haftmann, TU München
+                Florian Haftmann, TU Muenchen
 *)
 
 header {* Sublist Ordering *}
 
 theory Sublist_Order
-imports Plain "~~/src/HOL/List"
+imports Main
 begin
 
 text {*
diff -r 9ffd27558916 -r 0842e906300c src/HOL/Library/Univ_Poly.thy
--- a/src/HOL/Library/Univ_Poly.thy	Fri Mar 27 10:05:08 2009 +0100
+++ b/src/HOL/Library/Univ_Poly.thy	Fri Mar 27 10:05:11 2009 +0100
@@ -5,7 +5,7 @@
 header {* Univariate Polynomials *}
 
 theory Univ_Poly
-imports Plain List
+imports Main
 begin
 
 text{* Application of polynomial as a function. *}
diff -r 9ffd27558916 -r 0842e906300c src/HOL/Library/While_Combinator.thy
--- a/src/HOL/Library/While_Combinator.thy	Fri Mar 27 10:05:08 2009 +0100
+++ b/src/HOL/Library/While_Combinator.thy	Fri Mar 27 10:05:11 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Library/While_Combinator.thy
-    ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   2000 TU Muenchen
 *)
@@ -7,7 +6,7 @@
 header {* A general ``while'' combinator *}
 
 theory While_Combinator
-imports Plain "~~/src/HOL/Presburger"
+imports Main
 begin
 
 text {* 
diff -r 9ffd27558916 -r 0842e906300c src/HOL/Lubs.thy
--- a/src/HOL/Lubs.thy	Fri Mar 27 10:05:08 2009 +0100
+++ b/src/HOL/Lubs.thy	Fri Mar 27 10:05:11 2009 +0100
@@ -6,7 +6,7 @@
 header{*Definitions of Upper Bounds and Least Upper Bounds*}
 
 theory Lubs
-imports Plain Main
+imports Main
 begin
 
 text{*Thanks to suggestions by James Margetson*}
diff -r 9ffd27558916 -r 0842e906300c src/HOL/Map.thy
--- a/src/HOL/Map.thy	Fri Mar 27 10:05:08 2009 +0100
+++ b/src/HOL/Map.thy	Fri Mar 27 10:05:11 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Map.thy
-    ID:         $Id$
     Author:     Tobias Nipkow, based on a theory by David von Oheimb
     Copyright   1997-2003 TU Muenchen
 
diff -r 9ffd27558916 -r 0842e906300c src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Fri Mar 27 10:05:08 2009 +0100
+++ b/src/HOL/Parity.thy	Fri Mar 27 10:05:11 2009 +0100
@@ -5,7 +5,7 @@
 header {* Even and Odd for int and nat *}
 
 theory Parity
-imports Plain Presburger Main
+imports Main
 begin
 
 class even_odd =