normalized imports
authorhaftmann
Fri Mar 27 10:05:11 2009 +0100 (2009-03-27)
changeset 307380842e906300c
parent 30737 9ffd27558916
child 30739 8a854c90f7e6
normalized imports
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/GCD.thy
src/HOL/Imperative_HOL/Heap.thy
src/HOL/Library/Permutation.thy
src/HOL/Library/Pocklington.thy
src/HOL/Library/Polynomial.thy
src/HOL/Library/Primes.thy
src/HOL/Library/Product_ord.thy
src/HOL/Library/Quicksort.thy
src/HOL/Library/Quotient.thy
src/HOL/Library/RBT.thy
src/HOL/Library/Ramsey.thy
src/HOL/Library/SetsAndFunctions.thy
src/HOL/Library/State_Monad.thy
src/HOL/Library/Sublist_Order.thy
src/HOL/Library/Univ_Poly.thy
src/HOL/Library/While_Combinator.thy
src/HOL/Lubs.thy
src/HOL/Map.thy
src/HOL/Parity.thy
     1.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Fri Mar 27 10:05:08 2009 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Fri Mar 27 10:05:11 2009 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4    and a quantifier elimination procedure in Ferrante and Rackoff style *}
     1.5  
     1.6  theory Dense_Linear_Order
     1.7 -imports Plain Groebner_Basis Main
     1.8 +imports Main
     1.9  uses
    1.10    "~~/src/HOL/Tools/Qelim/langford_data.ML"
    1.11    "~~/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML"
     2.1 --- a/src/HOL/GCD.thy	Fri Mar 27 10:05:08 2009 +0100
     2.2 +++ b/src/HOL/GCD.thy	Fri Mar 27 10:05:11 2009 +0100
     2.3 @@ -6,7 +6,7 @@
     2.4  header {* The Greatest Common Divisor *}
     2.5  
     2.6  theory GCD
     2.7 -imports Plain Presburger Main
     2.8 +imports Main
     2.9  begin
    2.10  
    2.11  text {*
     3.1 --- a/src/HOL/Imperative_HOL/Heap.thy	Fri Mar 27 10:05:08 2009 +0100
     3.2 +++ b/src/HOL/Imperative_HOL/Heap.thy	Fri Mar 27 10:05:11 2009 +0100
     3.3 @@ -1,12 +1,11 @@
     3.4  (*  Title:      HOL/Library/Heap.thy
     3.5 -    ID:         $Id$
     3.6      Author:     John Matthews, Galois Connections; Alexander Krauss, TU Muenchen
     3.7  *)
     3.8  
     3.9  header {* A polymorphic heap based on cantor encodings *}
    3.10  
    3.11  theory Heap
    3.12 -imports Plain "~~/src/HOL/List" Countable Typerep
    3.13 +imports Main Countable
    3.14  begin
    3.15  
    3.16  subsection {* Representable types *}
     4.1 --- a/src/HOL/Library/Permutation.thy	Fri Mar 27 10:05:08 2009 +0100
     4.2 +++ b/src/HOL/Library/Permutation.thy	Fri Mar 27 10:05:11 2009 +0100
     4.3 @@ -5,7 +5,7 @@
     4.4  header {* Permutations *}
     4.5  
     4.6  theory Permutation
     4.7 -imports Plain Multiset
     4.8 +imports Main Multiset
     4.9  begin
    4.10  
    4.11  inductive
     5.1 --- a/src/HOL/Library/Pocklington.thy	Fri Mar 27 10:05:08 2009 +0100
     5.2 +++ b/src/HOL/Library/Pocklington.thy	Fri Mar 27 10:05:11 2009 +0100
     5.3 @@ -1,13 +1,11 @@
     5.4  (*  Title:      HOL/Library/Pocklington.thy
     5.5 -    ID:         $Id$
     5.6      Author:     Amine Chaieb
     5.7  *)
     5.8  
     5.9  header {* Pocklington's Theorem for Primes *}
    5.10  
    5.11 -
    5.12  theory Pocklington
    5.13 -imports Plain "~~/src/HOL/List" "~~/src/HOL/Primes"
    5.14 +imports Main Primes
    5.15  begin
    5.16  
    5.17  definition modeq:: "nat => nat => nat => bool"    ("(1[_ = _] '(mod _'))")
     6.1 --- a/src/HOL/Library/Polynomial.thy	Fri Mar 27 10:05:08 2009 +0100
     6.2 +++ b/src/HOL/Library/Polynomial.thy	Fri Mar 27 10:05:11 2009 +0100
     6.3 @@ -6,7 +6,7 @@
     6.4  header {* Univariate Polynomials *}
     6.5  
     6.6  theory Polynomial
     6.7 -imports Plain SetInterval Main
     6.8 +imports Main
     6.9  begin
    6.10  
    6.11  subsection {* Definition of type @{text poly} *}
     7.1 --- a/src/HOL/Library/Primes.thy	Fri Mar 27 10:05:08 2009 +0100
     7.2 +++ b/src/HOL/Library/Primes.thy	Fri Mar 27 10:05:11 2009 +0100
     7.3 @@ -6,7 +6,7 @@
     7.4  header {* Primality on nat *}
     7.5  
     7.6  theory Primes
     7.7 -imports Plain "~~/src/HOL/ATP_Linkup" "~~/src/HOL/GCD" "~~/src/HOL/Parity"
     7.8 +imports Complex_Main
     7.9  begin
    7.10  
    7.11  definition
     8.1 --- a/src/HOL/Library/Product_ord.thy	Fri Mar 27 10:05:08 2009 +0100
     8.2 +++ b/src/HOL/Library/Product_ord.thy	Fri Mar 27 10:05:11 2009 +0100
     8.3 @@ -1,12 +1,11 @@
     8.4  (*  Title:      HOL/Library/Product_ord.thy
     8.5 -    ID:         $Id$
     8.6      Author:     Norbert Voelker
     8.7  *)
     8.8  
     8.9  header {* Order on product types *}
    8.10  
    8.11  theory Product_ord
    8.12 -imports Plain
    8.13 +imports Main
    8.14  begin
    8.15  
    8.16  instantiation "*" :: (ord, ord) ord
     9.1 --- a/src/HOL/Library/Quicksort.thy	Fri Mar 27 10:05:08 2009 +0100
     9.2 +++ b/src/HOL/Library/Quicksort.thy	Fri Mar 27 10:05:11 2009 +0100
     9.3 @@ -1,12 +1,11 @@
     9.4 -(*  ID:         $Id$
     9.5 -    Author:     Tobias Nipkow
     9.6 +(*  Author:     Tobias Nipkow
     9.7      Copyright   1994 TU Muenchen
     9.8  *)
     9.9  
    9.10  header{*Quicksort*}
    9.11  
    9.12  theory Quicksort
    9.13 -imports Plain Multiset
    9.14 +imports Main Multiset
    9.15  begin
    9.16  
    9.17  context linorder
    10.1 --- a/src/HOL/Library/Quotient.thy	Fri Mar 27 10:05:08 2009 +0100
    10.2 +++ b/src/HOL/Library/Quotient.thy	Fri Mar 27 10:05:11 2009 +0100
    10.3 @@ -1,12 +1,11 @@
    10.4  (*  Title:      HOL/Library/Quotient.thy
    10.5 -    ID:         $Id$
    10.6      Author:     Markus Wenzel, TU Muenchen
    10.7  *)
    10.8  
    10.9  header {* Quotient types *}
   10.10  
   10.11  theory Quotient
   10.12 -imports Plain "~~/src/HOL/Hilbert_Choice"
   10.13 +imports Main
   10.14  begin
   10.15  
   10.16  text {*
    11.1 --- a/src/HOL/Library/RBT.thy	Fri Mar 27 10:05:08 2009 +0100
    11.2 +++ b/src/HOL/Library/RBT.thy	Fri Mar 27 10:05:11 2009 +0100
    11.3 @@ -1,5 +1,4 @@
    11.4  (*  Title:      RBT.thy
    11.5 -    ID:         $Id$
    11.6      Author:     Markus Reiter, TU Muenchen
    11.7      Author:     Alexander Krauss, TU Muenchen
    11.8  *)
    11.9 @@ -8,7 +7,7 @@
   11.10  
   11.11  (*<*)
   11.12  theory RBT
   11.13 -imports Plain AssocList
   11.14 +imports Main AssocList
   11.15  begin
   11.16  
   11.17  datatype color = R | B
    12.1 --- a/src/HOL/Library/Ramsey.thy	Fri Mar 27 10:05:08 2009 +0100
    12.2 +++ b/src/HOL/Library/Ramsey.thy	Fri Mar 27 10:05:11 2009 +0100
    12.3 @@ -1,12 +1,11 @@
    12.4  (*  Title:      HOL/Library/Ramsey.thy
    12.5 -    ID:         $Id$
    12.6      Author:     Tom Ridge. Converted to structured Isar by L C Paulson
    12.7  *)
    12.8  
    12.9  header "Ramsey's Theorem"
   12.10  
   12.11  theory Ramsey
   12.12 -imports Plain "~~/src/HOL/Presburger" Infinite_Set
   12.13 +imports Main Infinite_Set
   12.14  begin
   12.15  
   12.16  subsection {* Preliminaries *}
    13.1 --- a/src/HOL/Library/SetsAndFunctions.thy	Fri Mar 27 10:05:08 2009 +0100
    13.2 +++ b/src/HOL/Library/SetsAndFunctions.thy	Fri Mar 27 10:05:11 2009 +0100
    13.3 @@ -5,7 +5,7 @@
    13.4  header {* Operations on sets and functions *}
    13.5  
    13.6  theory SetsAndFunctions
    13.7 -imports Plain
    13.8 +imports Main
    13.9  begin
   13.10  
   13.11  text {*
    14.1 --- a/src/HOL/Library/State_Monad.thy	Fri Mar 27 10:05:08 2009 +0100
    14.2 +++ b/src/HOL/Library/State_Monad.thy	Fri Mar 27 10:05:11 2009 +0100
    14.3 @@ -5,7 +5,7 @@
    14.4  header {* Combinator syntax for generic, open state monads (single threaded monads) *}
    14.5  
    14.6  theory State_Monad
    14.7 -imports Plain "~~/src/HOL/List"
    14.8 +imports Main
    14.9  begin
   14.10  
   14.11  subsection {* Motivation *}
    15.1 --- a/src/HOL/Library/Sublist_Order.thy	Fri Mar 27 10:05:08 2009 +0100
    15.2 +++ b/src/HOL/Library/Sublist_Order.thy	Fri Mar 27 10:05:11 2009 +0100
    15.3 @@ -1,13 +1,12 @@
    15.4  (*  Title:      HOL/Library/Sublist_Order.thy
    15.5 -    ID:         $Id$
    15.6      Authors:    Peter Lammich, Uni Muenster <peter.lammich@uni-muenster.de>
    15.7 -                Florian Haftmann, TU M√ľnchen
    15.8 +                Florian Haftmann, TU Muenchen
    15.9  *)
   15.10  
   15.11  header {* Sublist Ordering *}
   15.12  
   15.13  theory Sublist_Order
   15.14 -imports Plain "~~/src/HOL/List"
   15.15 +imports Main
   15.16  begin
   15.17  
   15.18  text {*
    16.1 --- a/src/HOL/Library/Univ_Poly.thy	Fri Mar 27 10:05:08 2009 +0100
    16.2 +++ b/src/HOL/Library/Univ_Poly.thy	Fri Mar 27 10:05:11 2009 +0100
    16.3 @@ -5,7 +5,7 @@
    16.4  header {* Univariate Polynomials *}
    16.5  
    16.6  theory Univ_Poly
    16.7 -imports Plain List
    16.8 +imports Main
    16.9  begin
   16.10  
   16.11  text{* Application of polynomial as a function. *}
    17.1 --- a/src/HOL/Library/While_Combinator.thy	Fri Mar 27 10:05:08 2009 +0100
    17.2 +++ b/src/HOL/Library/While_Combinator.thy	Fri Mar 27 10:05:11 2009 +0100
    17.3 @@ -1,5 +1,4 @@
    17.4  (*  Title:      HOL/Library/While_Combinator.thy
    17.5 -    ID:         $Id$
    17.6      Author:     Tobias Nipkow
    17.7      Copyright   2000 TU Muenchen
    17.8  *)
    17.9 @@ -7,7 +6,7 @@
   17.10  header {* A general ``while'' combinator *}
   17.11  
   17.12  theory While_Combinator
   17.13 -imports Plain "~~/src/HOL/Presburger"
   17.14 +imports Main
   17.15  begin
   17.16  
   17.17  text {* 
    18.1 --- a/src/HOL/Lubs.thy	Fri Mar 27 10:05:08 2009 +0100
    18.2 +++ b/src/HOL/Lubs.thy	Fri Mar 27 10:05:11 2009 +0100
    18.3 @@ -6,7 +6,7 @@
    18.4  header{*Definitions of Upper Bounds and Least Upper Bounds*}
    18.5  
    18.6  theory Lubs
    18.7 -imports Plain Main
    18.8 +imports Main
    18.9  begin
   18.10  
   18.11  text{*Thanks to suggestions by James Margetson*}
    19.1 --- a/src/HOL/Map.thy	Fri Mar 27 10:05:08 2009 +0100
    19.2 +++ b/src/HOL/Map.thy	Fri Mar 27 10:05:11 2009 +0100
    19.3 @@ -1,5 +1,4 @@
    19.4  (*  Title:      HOL/Map.thy
    19.5 -    ID:         $Id$
    19.6      Author:     Tobias Nipkow, based on a theory by David von Oheimb
    19.7      Copyright   1997-2003 TU Muenchen
    19.8  
    20.1 --- a/src/HOL/Parity.thy	Fri Mar 27 10:05:08 2009 +0100
    20.2 +++ b/src/HOL/Parity.thy	Fri Mar 27 10:05:11 2009 +0100
    20.3 @@ -5,7 +5,7 @@
    20.4  header {* Even and Odd for int and nat *}
    20.5  
    20.6  theory Parity
    20.7 -imports Plain Presburger Main
    20.8 +imports Main
    20.9  begin
   20.10  
   20.11  class even_odd =