--- 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"
--- 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 {*
--- 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 *}
--- 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
--- 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 _'))")
--- 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} *}
--- 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
--- 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
--- 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
--- 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 {*
--- 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
--- 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 *}
--- 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 {*
--- 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 *}
--- 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 {*
--- 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. *}
--- 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 {*
--- 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*}
--- 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
--- 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 =