# HG changeset patch
# User haftmann
# Date 1237792584 -3600
# Node ID 4cf38ea4fad2416168c1a5a15f28db569bfb137c
# Parent  a400b06d03cbfc6546fc35d5340b7170b599844d# Parent  167da873c3b347a76b4f34e79c6b9d0e746981a6
merged

diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Import/HOL4Compat.thy
--- a/src/HOL/Import/HOL4Compat.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Import/HOL4Compat.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -1,11 +1,14 @@
 (*  Title:      HOL/Import/HOL4Compat.thy
-    ID:         $Id$
     Author:     Sebastian Skalberg (TU Muenchen)
 *)
 
-theory HOL4Compat imports HOL4Setup Divides Primes Real ContNotDenum
+theory HOL4Compat
+imports HOL4Setup Complex_Main Primes ContNotDenum
 begin
 
+no_notation differentiable (infixl "differentiable" 60)
+no_notation sums (infixr "sums" 80)
+
 lemma EXISTS_UNIQUE_DEF: "(Ex1 P) = (Ex P & (ALL x y. P x & P y --> (x = y)))"
   by auto
 
@@ -22,7 +25,7 @@
 lemmas [hol4rew] = ONE_ONE_rew
 
 lemma bool_case_DEF: "(bool_case x y b) = (if b then x else y)"
-  by simp;
+  by simp
 
 lemma INR_INL_11: "(ALL y x. (Inl x = Inl y) = (x = y)) & (ALL y x. (Inr x = Inr y) = (x = y))"
   by safe
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Abstract_Rat.thy
--- a/src/HOL/Library/Abstract_Rat.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Abstract_Rat.thy	Mon Mar 23 08:16: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"
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/AssocList.thy
--- a/src/HOL/Library/AssocList.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/AssocList.thy	Mon Mar 23 08:16: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 {*
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Binomial.thy
--- a/src/HOL/Library/Binomial.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Binomial.thy	Mon Mar 23 08:16: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
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Boolean_Algebra.thy
--- a/src/HOL/Library/Boolean_Algebra.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Boolean_Algebra.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -5,7 +5,7 @@
 header {* Boolean Algebras *}
 
 theory Boolean_Algebra
-imports Plain
+imports Main
 begin
 
 locale boolean =
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Char_nat.thy
--- a/src/HOL/Library/Char_nat.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Char_nat.thy	Mon Mar 23 08:16: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]. *}
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Char_ord.thy
--- a/src/HOL/Library/Char_ord.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Char_ord.thy	Mon Mar 23 08:16: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
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Code_Char.thy
--- a/src/HOL/Library/Code_Char.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Code_Char.thy	Mon Mar 23 08:16: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
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Code_Char_chr.thy
--- a/src/HOL/Library/Code_Char_chr.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Code_Char_chr.thy	Mon Mar 23 08:16: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
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Code_Index.thy
--- a/src/HOL/Library/Code_Index.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Code_Index.thy	Mon Mar 23 08:16: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 {*
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Code_Integer.thy
--- a/src/HOL/Library/Code_Integer.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Code_Integer.thy	Mon Mar 23 08:16: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 {*
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Coinductive_List.thy
--- a/src/HOL/Library/Coinductive_List.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Coinductive_List.thy	Mon Mar 23 08:16: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 *}
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Commutative_Ring.thy
--- a/src/HOL/Library/Commutative_Ring.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Commutative_Ring.thy	Mon Mar 23 08:16: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
 
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/ContNotDenum.thy
--- a/src/HOL/Library/ContNotDenum.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/ContNotDenum.thy	Mon Mar 23 08:16: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 *}
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Continuity.thy
--- a/src/HOL/Library/Continuity.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Continuity.thy	Mon Mar 23 08:16: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 *}
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Countable.thy	Mon Mar 23 08:16: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 *}
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Determinants.thy
--- a/src/HOL/Library/Determinants.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Determinants.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -5,7 +5,7 @@
 header {* Traces, Determinant of square matrices and some properties *}
 
 theory Determinants
-  imports Euclidean_Space Permutations
+imports Euclidean_Space Permutations
 begin
 
 subsection{* First some facts about products*}
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Mon Mar 23 08:16: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 {*
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Enum.thy
--- a/src/HOL/Library/Enum.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Enum.thy	Mon Mar 23 08:16: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} *}
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Euclidean_Space.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -5,7 +5,8 @@
 header {* (Real) Vectors in Euclidean space, and elementary linear algebra.*}
 
 theory Euclidean_Space
-imports Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
+imports
+  Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
   Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type
   Inner_Product
 uses ("normarith.ML")
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Eval_Witness.thy
--- a/src/HOL/Library/Eval_Witness.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Eval_Witness.thy	Mon Mar 23 08:16: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 {* 
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Executable_Set.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      HOL/Library/Executable_Set.thy
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen
 *)
 
 header {* Implementation of finite sets by lists *}
 
 theory Executable_Set
-imports Plain "~~/src/HOL/List"
+imports Main
 begin
 
 subsection {* Definitional rewrites *}
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Finite_Cartesian_Product.thy
--- a/src/HOL/Library/Finite_Cartesian_Product.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Finite_Cartesian_Product.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -5,12 +5,9 @@
 header {* Definition of finite Cartesian product types. *}
 
 theory Finite_Cartesian_Product
-  (* imports Plain SetInterval ATP_Linkup *)
-imports Main
+imports Main (*FIXME: ATP_Linkup is only needed for metis at a few places. We could dispense of that by changing the proofs.*)
 begin
 
-  (* FIXME : ATP_Linkup is only needed for metis at a few places. We could dispense of that by changing the proofs*)
-
 definition hassize (infixr "hassize" 12) where
   "(S hassize n) = (finite S \<and> card S = n)"
 
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -1,12 +1,11 @@
 (*  Title:      Formal_Power_Series.thy
-    ID:
     Author:     Amine Chaieb, University of Cambridge
 *)
 
 header{* A formalization of formal power series *}
 
 theory Formal_Power_Series
-  imports Main Fact Parity
+imports Main Fact Parity
 begin
 
 subsection {* The type of formal power series*}
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/FrechetDeriv.thy
--- a/src/HOL/Library/FrechetDeriv.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/FrechetDeriv.thy	Mon Mar 23 08:16: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
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/FuncSet.thy	Mon Mar 23 08:16: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
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Glbs.thy
--- a/src/HOL/Library/Glbs.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Glbs.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -1,8 +1,6 @@
-(* Title:      Glbs
-   Author:     Amine Chaieb, University of Cambridge
-*)
+(* Author: Amine Chaieb, University of Cambridge *)
 
-header{*Definitions of Lower Bounds and Greatest Lower Bounds, analogous to Lubs*}
+header {* Definitions of Lower Bounds and Greatest Lower Bounds, analogous to Lubs *}
 
 theory Glbs
 imports Lubs
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Mon Mar 23 08:16: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 {*
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Inner_Product.thy
--- a/src/HOL/Library/Inner_Product.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Inner_Product.thy	Mon Mar 23 08:16: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 *}
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/LaTeXsugar.thy
--- a/src/HOL/Library/LaTeXsugar.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -5,7 +5,7 @@
 
 (*<*)
 theory LaTeXsugar
-imports Plain "~~/src/HOL/List"
+imports Main
 begin
 
 (* LOGIC *)
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/ListVector.thy
--- a/src/HOL/Library/ListVector.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/ListVector.thy	Mon Mar 23 08:16: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
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/List_Prefix.thy
--- a/src/HOL/Library/List_Prefix.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/List_Prefix.thy	Mon Mar 23 08:16: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 *}
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/List_lexord.thy
--- a/src/HOL/Library/List_lexord.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/List_lexord.thy	Mon Mar 23 08:16: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
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Mapping.thy	Mon Mar 23 08:16: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 *}
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Multiset.thy	Mon Mar 23 08:16: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 *}
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Nat_Infinity.thy
--- a/src/HOL/Library/Nat_Infinity.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Nat_Infinity.thy	Mon Mar 23 08:16: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 *}
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Nat_Int_Bij.thy
--- a/src/HOL/Library/Nat_Int_Bij.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Nat_Int_Bij.thy	Mon Mar 23 08:16: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>"} *}
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Nested_Environment.thy
--- a/src/HOL/Library/Nested_Environment.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Nested_Environment.thy	Mon Mar 23 08:16: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 {*
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Numeral_Type.thy	Mon Mar 23 08:16: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 *}
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Option_ord.thy
--- a/src/HOL/Library/Option_ord.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Option_ord.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -1,15 +1,14 @@
 (*  Title:      HOL/Library/Option_ord.thy
-    ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 *)
 
 header {* Canonical order on option type *}
 
 theory Option_ord
-imports Plain
+imports Option Main
 begin
 
-instantiation option :: (order) order
+instantiation option :: (preorder) preorder
 begin
 
 definition less_eq_option where
@@ -48,12 +47,63 @@
 lemma less_option_Some [simp, code]: "Some x < Some y \<longleftrightarrow> x < y"
   by (simp add: less_option_def)
 
-instance by default
-  (auto simp add: less_eq_option_def less_option_def split: option.splits)
+instance proof
+qed (auto simp add: less_eq_option_def less_option_def less_le_not_le elim: order_trans split: option.splits)
 
 end 
 
-instance option :: (linorder) linorder
-  by default (auto simp add: less_eq_option_def less_option_def split: option.splits)
+instance option :: (order) order proof
+qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
+
+instance option :: (linorder) linorder proof
+qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
+
+instantiation option :: (preorder) bot
+begin
+
+definition "bot = None"
+
+instance proof
+qed (simp add: bot_option_def)
+
+end
+
+instantiation option :: (top) top
+begin
+
+definition "top = Some top"
+
+instance proof
+qed (simp add: top_option_def less_eq_option_def split: option.split)
 
 end
+
+instance option :: (wellorder) wellorder proof
+  fix P :: "'a option \<Rightarrow> bool" and z :: "'a option"
+  assume H: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
+  have "P None" by (rule H) simp
+  then have P_Some [case_names Some]:
+    "\<And>z. (\<And>x. z = Some x \<Longrightarrow> (P o Some) x) \<Longrightarrow> P z"
+  proof -
+    fix z
+    assume "\<And>x. z = Some x \<Longrightarrow> (P o Some) x"
+    with `P None` show "P z" by (cases z) simp_all
+  qed
+  show "P z" proof (cases z rule: P_Some)
+    case (Some w)
+    show "(P o Some) w" proof (induct rule: less_induct)
+      case (less x)
+      have "P (Some x)" proof (rule H)
+        fix y :: "'a option"
+        assume "y < Some x"
+        show "P y" proof (cases y rule: P_Some)
+          case (Some v) with `y < Some x` have "v < x" by simp
+          with less show "(P o Some) v" .
+        qed
+      qed
+      then show ?case by simp
+    qed
+  qed
+qed
+
+end
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/OptionalSugar.thy
--- a/src/HOL/Library/OptionalSugar.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/OptionalSugar.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -4,7 +4,7 @@
 *)
 (*<*)
 theory OptionalSugar
-imports LaTeXsugar Complex_Main
+imports Complex_Main LaTeXsugar
 begin
 
 (* hiding set *)
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Order_Relation.thy
--- a/src/HOL/Library/Order_Relation.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Order_Relation.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -1,6 +1,4 @@
-(*  ID          : $Id$
-    Author      : Tobias Nipkow
-*)
+(* Author: Tobias Nipkow *)
 
 header {* Orders as Relations *}
 
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Permutations.thy
--- a/src/HOL/Library/Permutations.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Permutations.thy	Mon Mar 23 08:16: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! *)
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Zorn.thy
--- a/src/HOL/Library/Zorn.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/Library/Zorn.thy	Mon Mar 23 08:16: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? *)
diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/ex/MergeSort.thy
--- a/src/HOL/ex/MergeSort.thy	Mon Mar 23 07:41:07 2009 +0100
+++ b/src/HOL/ex/MergeSort.thy	Mon Mar 23 08:16:24 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/ex/Merge.thy
-    ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   2002 TU Muenchen
 *)