--- a/src/HOL/Library/Abstract_Rat.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/Abstract_Rat.thy Mon Mar 23 08:14:24 2009 +0100
@@ -1,12 +1,11 @@
(* Title: HOL/Library/Abstract_Rat.thy
- ID: $Id$
Author: Amine Chaieb
*)
header {* Abstract rational numbers *}
theory Abstract_Rat
-imports Plain GCD
+imports GCD Main
begin
types Num = "int \<times> int"
--- a/src/HOL/Library/AssocList.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/AssocList.thy Mon Mar 23 08:14:24 2009 +0100
@@ -1,12 +1,11 @@
(* Title: HOL/Library/AssocList.thy
- ID: $Id$
Author: Norbert Schirmer, Tobias Nipkow, Martin Wildmoser
*)
header {* Map operations implemented on association lists*}
theory AssocList
-imports Plain "~~/src/HOL/Map"
+imports Map Main
begin
text {*
--- a/src/HOL/Library/Binomial.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/Binomial.thy Mon Mar 23 08:14:24 2009 +0100
@@ -6,7 +6,7 @@
header {* Binomial Coefficients *}
theory Binomial
-imports Fact Plain "~~/src/HOL/SetInterval" Presburger
+imports Fact SetInterval Presburger Main
begin
text {* This development is based on the work of Andy Gordon and
--- a/src/HOL/Library/Boolean_Algebra.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/Boolean_Algebra.thy Mon Mar 23 08:14:24 2009 +0100
@@ -5,7 +5,7 @@
header {* Boolean Algebras *}
theory Boolean_Algebra
-imports Plain
+imports Main
begin
locale boolean =
--- a/src/HOL/Library/Char_nat.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/Char_nat.thy Mon Mar 23 08:14:24 2009 +0100
@@ -1,12 +1,11 @@
(* Title: HOL/Library/Char_nat.thy
- ID: $Id$
Author: Norbert Voelker, Florian Haftmann
*)
header {* Mapping between characters and natural numbers *}
theory Char_nat
-imports Plain "~~/src/HOL/List"
+imports List Main
begin
text {* Conversions between nibbles and natural numbers in [0..15]. *}
--- a/src/HOL/Library/Char_ord.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/Char_ord.thy Mon Mar 23 08:14:24 2009 +0100
@@ -1,12 +1,11 @@
(* Title: HOL/Library/Char_ord.thy
- ID: $Id$
Author: Norbert Voelker, Florian Haftmann
*)
header {* Order on characters *}
theory Char_ord
-imports Plain Product_ord Char_nat
+imports Product_ord Char_nat Main
begin
instantiation nibble :: linorder
--- a/src/HOL/Library/Code_Char.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/Code_Char.thy Mon Mar 23 08:14:24 2009 +0100
@@ -5,7 +5,7 @@
header {* Code generation of pretty characters (and strings) *}
theory Code_Char
-imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Eval"
+imports List Code_Eval Main
begin
code_type char
--- a/src/HOL/Library/Code_Char_chr.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/Code_Char_chr.thy Mon Mar 23 08:14:24 2009 +0100
@@ -1,12 +1,11 @@
(* Title: HOL/Library/Code_Char_chr.thy
- ID: $Id$
Author: Florian Haftmann
*)
header {* Code generation of pretty characters with character codes *}
theory Code_Char_chr
-imports Plain Char_nat Code_Char Code_Integer
+imports Char_nat Code_Char Code_Integer Main
begin
definition
--- a/src/HOL/Library/Code_Index.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/Code_Index.thy Mon Mar 23 08:14:24 2009 +0100
@@ -3,7 +3,7 @@
header {* Type of indices *}
theory Code_Index
-imports Plain "~~/src/HOL/Code_Eval" "~~/src/HOL/Presburger"
+imports Main
begin
text {*
--- a/src/HOL/Library/Code_Integer.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/Code_Integer.thy Mon Mar 23 08:14:24 2009 +0100
@@ -5,7 +5,7 @@
header {* Pretty integer literals for code generation *}
theory Code_Integer
-imports Plain "~~/src/HOL/Code_Eval" "~~/src/HOL/Presburger"
+imports Main
begin
text {*
--- a/src/HOL/Library/Coinductive_List.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/Coinductive_List.thy Mon Mar 23 08:14:24 2009 +0100
@@ -1,12 +1,11 @@
(* Title: HOL/Library/Coinductive_Lists.thy
- ID: $Id$
Author: Lawrence C Paulson and Makarius
*)
header {* Potentially infinite lists as greatest fixed-point *}
theory Coinductive_List
-imports Plain "~~/src/HOL/List"
+imports List Main
begin
subsection {* List constructors over the datatype universe *}
--- a/src/HOL/Library/Commutative_Ring.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/Commutative_Ring.thy Mon Mar 23 08:14:24 2009 +0100
@@ -6,7 +6,7 @@
header {* Proving equalities in commutative rings *}
theory Commutative_Ring
-imports Plain "~~/src/HOL/List" "~~/src/HOL/Parity"
+imports List Parity Main
uses ("comm_ring.ML")
begin
--- a/src/HOL/Library/ContNotDenum.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/ContNotDenum.thy Mon Mar 23 08:14:24 2009 +0100
@@ -5,7 +5,7 @@
header {* Non-denumerability of the Continuum. *}
theory ContNotDenum
-imports RComplete Hilbert_Choice
+imports Complex_Main
begin
subsection {* Abstract *}
--- a/src/HOL/Library/Continuity.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/Continuity.thy Mon Mar 23 08:14:24 2009 +0100
@@ -1,12 +1,11 @@
(* Title: HOL/Library/Continuity.thy
- ID: $Id$
Author: David von Oheimb, TU Muenchen
*)
header {* Continuity and iterations (of set transformers) *}
theory Continuity
-imports Plain "~~/src/HOL/Relation_Power"
+imports Relation_Power Main
begin
subsection {* Continuity for complete lattices *}
--- a/src/HOL/Library/Countable.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/Countable.thy Mon Mar 23 08:14:24 2009 +0100
@@ -6,11 +6,11 @@
theory Countable
imports
- Plain
"~~/src/HOL/List"
"~~/src/HOL/Hilbert_Choice"
"~~/src/HOL/Nat_Int_Bij"
"~~/src/HOL/Rational"
+ Main
begin
subsection {* The class of countable types *}
--- a/src/HOL/Library/Efficient_Nat.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy Mon Mar 23 08:14:24 2009 +0100
@@ -5,7 +5,7 @@
header {* Implementation of natural numbers by target-language integers *}
theory Efficient_Nat
-imports Code_Index Code_Integer
+imports Code_Index Code_Integer Main
begin
text {*
--- a/src/HOL/Library/Enum.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/Enum.thy Mon Mar 23 08:14:24 2009 +0100
@@ -5,7 +5,7 @@
header {* Finite types as explicit enumerations *}
theory Enum
-imports Plain "~~/src/HOL/Map"
+imports Map Main
begin
subsection {* Class @{text enum} *}
--- a/src/HOL/Library/Eval_Witness.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/Eval_Witness.thy Mon Mar 23 08:14:24 2009 +0100
@@ -5,7 +5,7 @@
header {* Evaluation Oracle with ML witnesses *}
theory Eval_Witness
-imports Plain "~~/src/HOL/List"
+imports List Main
begin
text {*
--- a/src/HOL/Library/FrechetDeriv.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/FrechetDeriv.thy Mon Mar 23 08:14:24 2009 +0100
@@ -1,12 +1,11 @@
(* Title : FrechetDeriv.thy
- ID : $Id$
Author : Brian Huffman
*)
header {* Frechet Derivative *}
theory FrechetDeriv
-imports Lim
+imports Lim Complex_Main
begin
definition
--- a/src/HOL/Library/FuncSet.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/FuncSet.thy Mon Mar 23 08:14:24 2009 +0100
@@ -1,12 +1,11 @@
(* Title: HOL/Library/FuncSet.thy
- ID: $Id$
Author: Florian Kammueller and Lawrence C Paulson
*)
header {* Pi and Function Sets *}
theory FuncSet
-imports Plain "~~/src/HOL/Hilbert_Choice"
+imports Hilbert_Choice Main
begin
definition
--- a/src/HOL/Library/Infinite_Set.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/Infinite_Set.thy Mon Mar 23 08:14:24 2009 +0100
@@ -1,15 +1,13 @@
(* Title: HOL/Library/Infinite_Set.thy
- ID: $Id$
Author: Stephan Merz
*)
header {* Infinite Sets and Related Concepts *}
theory Infinite_Set
-imports Main "~~/src/HOL/SetInterval" "~~/src/HOL/Hilbert_Choice"
+imports Main
begin
-
subsection "Infinite Sets"
text {*
--- a/src/HOL/Library/Inner_Product.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/Inner_Product.thy Mon Mar 23 08:14:24 2009 +0100
@@ -5,7 +5,7 @@
header {* Inner Product Spaces and the Gradient Derivative *}
theory Inner_Product
-imports Complex FrechetDeriv
+imports Complex_Main FrechetDeriv
begin
subsection {* Real inner product spaces *}
--- a/src/HOL/Library/LaTeXsugar.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy Mon Mar 23 08:14:24 2009 +0100
@@ -5,7 +5,7 @@
(*<*)
theory LaTeXsugar
-imports Plain "~~/src/HOL/List"
+imports Main
begin
(* LOGIC *)
--- a/src/HOL/Library/ListVector.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/ListVector.thy Mon Mar 23 08:14:24 2009 +0100
@@ -1,11 +1,9 @@
-(* ID: $Id$
- Author: Tobias Nipkow, 2007
-*)
+(* Author: Tobias Nipkow, 2007 *)
-header "Lists as vectors"
+header {* Lists as vectors *}
theory ListVector
-imports Plain "~~/src/HOL/List"
+imports List Main
begin
text{* \noindent
--- a/src/HOL/Library/List_Prefix.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/List_Prefix.thy Mon Mar 23 08:14:24 2009 +0100
@@ -1,12 +1,11 @@
(* Title: HOL/Library/List_Prefix.thy
- ID: $Id$
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen
*)
header {* List prefixes and postfixes *}
theory List_Prefix
-imports Plain "~~/src/HOL/List"
+imports List Main
begin
subsection {* Prefix order on lists *}
--- a/src/HOL/Library/List_lexord.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/List_lexord.thy Mon Mar 23 08:14:24 2009 +0100
@@ -1,12 +1,11 @@
(* Title: HOL/Library/List_lexord.thy
- ID: $Id$
Author: Norbert Voelker
*)
header {* Lexicographic order on lists *}
theory List_lexord
-imports Plain "~~/src/HOL/List"
+imports List Main
begin
instantiation list :: (ord) ord
--- a/src/HOL/Library/Mapping.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/Mapping.thy Mon Mar 23 08:14:24 2009 +0100
@@ -5,7 +5,7 @@
header {* An abstract view on maps for code generation. *}
theory Mapping
-imports Map
+imports Map Main
begin
subsection {* Type definition and primitive operations *}
--- a/src/HOL/Library/Multiset.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/Multiset.thy Mon Mar 23 08:14:24 2009 +0100
@@ -5,7 +5,7 @@
header {* Multisets *}
theory Multiset
-imports Plain "~~/src/HOL/List"
+imports List Main
begin
subsection {* The type of multisets *}
--- a/src/HOL/Library/Nat_Infinity.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/Nat_Infinity.thy Mon Mar 23 08:14:24 2009 +0100
@@ -5,7 +5,7 @@
header {* Natural numbers with infinity *}
theory Nat_Infinity
-imports Plain "~~/src/HOL/Presburger"
+imports Main
begin
subsection {* Type definition *}
--- a/src/HOL/Library/Nat_Int_Bij.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/Nat_Int_Bij.thy Mon Mar 23 08:14:24 2009 +0100
@@ -1,12 +1,11 @@
(* Title: HOL/Nat_Int_Bij.thy
- ID: $Id$
Author: Stefan Richter, Tobias Nipkow
*)
header{* Bijections $\mathbb{N}\to\mathbb{N}^2$ and $\mathbb{N}\to\mathbb{Z}$*}
theory Nat_Int_Bij
-imports Hilbert_Choice Presburger
+imports Main
begin
subsection{* A bijection between @{text "\<nat>"} and @{text "\<nat>\<twosuperior>"} *}
--- a/src/HOL/Library/Nested_Environment.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/Nested_Environment.thy Mon Mar 23 08:14:24 2009 +0100
@@ -1,12 +1,11 @@
(* Title: HOL/Library/Nested_Environment.thy
- ID: $Id$
Author: Markus Wenzel, TU Muenchen
*)
header {* Nested environments *}
theory Nested_Environment
-imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Eval"
+imports Main
begin
text {*
--- a/src/HOL/Library/Numeral_Type.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/Numeral_Type.thy Mon Mar 23 08:14:24 2009 +0100
@@ -5,7 +5,7 @@
header {* Numeral Syntax for Types *}
theory Numeral_Type
-imports Plain "~~/src/HOL/Presburger"
+imports Main
begin
subsection {* Preliminary lemmas *}
--- a/src/HOL/Library/OptionalSugar.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/OptionalSugar.thy Mon Mar 23 08:14:24 2009 +0100
@@ -4,7 +4,7 @@
*)
(*<*)
theory OptionalSugar
-imports LaTeXsugar Complex_Main
+imports Complex_Main LaTeXsugar
begin
(* hiding set *)
--- a/src/HOL/Library/Permutations.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/Permutations.thy Mon Mar 23 08:14:24 2009 +0100
@@ -5,7 +5,7 @@
header {* Permutations, both general and specifically on finite sets.*}
theory Permutations
-imports Main Finite_Cartesian_Product Parity Fact
+imports Finite_Cartesian_Product Parity Fact Main
begin
(* Why should I import Main just to solve the Typerep problem! *)
--- a/src/HOL/Library/Zorn.thy Mon Mar 23 08:14:23 2009 +0100
+++ b/src/HOL/Library/Zorn.thy Mon Mar 23 08:14:24 2009 +0100
@@ -7,7 +7,7 @@
header {* Zorn's Lemma *}
theory Zorn
-imports "~~/src/HOL/Order_Relation"
+imports Order_Relation Main
begin
(* Define globally? In Set.thy? *)