merged
authorhaftmann
Mon Mar 23 08:16:24 2009 +0100 (2009-03-23)
changeset 306654cf38ea4fad2
parent 30659 a400b06d03cb
parent 30664 167da873c3b3
child 30666 d6248d4508d5
child 30684 c98a64746c69
child 30734 ab05be086c4a
merged
src/HOL/Library/Euclidean_Space.thy
     1.1 --- a/src/HOL/Import/HOL4Compat.thy	Mon Mar 23 07:41:07 2009 +0100
     1.2 +++ b/src/HOL/Import/HOL4Compat.thy	Mon Mar 23 08:16:24 2009 +0100
     1.3 @@ -1,11 +1,14 @@
     1.4  (*  Title:      HOL/Import/HOL4Compat.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Sebastian Skalberg (TU Muenchen)
     1.7  *)
     1.8  
     1.9 -theory HOL4Compat imports HOL4Setup Divides Primes Real ContNotDenum
    1.10 +theory HOL4Compat
    1.11 +imports HOL4Setup Complex_Main Primes ContNotDenum
    1.12  begin
    1.13  
    1.14 +no_notation differentiable (infixl "differentiable" 60)
    1.15 +no_notation sums (infixr "sums" 80)
    1.16 +
    1.17  lemma EXISTS_UNIQUE_DEF: "(Ex1 P) = (Ex P & (ALL x y. P x & P y --> (x = y)))"
    1.18    by auto
    1.19  
    1.20 @@ -22,7 +25,7 @@
    1.21  lemmas [hol4rew] = ONE_ONE_rew
    1.22  
    1.23  lemma bool_case_DEF: "(bool_case x y b) = (if b then x else y)"
    1.24 -  by simp;
    1.25 +  by simp
    1.26  
    1.27  lemma INR_INL_11: "(ALL y x. (Inl x = Inl y) = (x = y)) & (ALL y x. (Inr x = Inr y) = (x = y))"
    1.28    by safe
     2.1 --- a/src/HOL/Library/Abstract_Rat.thy	Mon Mar 23 07:41:07 2009 +0100
     2.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Mon Mar 23 08:16:24 2009 +0100
     2.3 @@ -1,12 +1,11 @@
     2.4  (*  Title:      HOL/Library/Abstract_Rat.thy
     2.5 -    ID:         $Id$
     2.6      Author:     Amine Chaieb
     2.7  *)
     2.8  
     2.9  header {* Abstract rational numbers *}
    2.10  
    2.11  theory Abstract_Rat
    2.12 -imports Plain GCD
    2.13 +imports GCD Main
    2.14  begin
    2.15  
    2.16  types Num = "int \<times> int"
     3.1 --- a/src/HOL/Library/AssocList.thy	Mon Mar 23 07:41:07 2009 +0100
     3.2 +++ b/src/HOL/Library/AssocList.thy	Mon Mar 23 08:16:24 2009 +0100
     3.3 @@ -1,12 +1,11 @@
     3.4  (*  Title:      HOL/Library/AssocList.thy
     3.5 -    ID:         $Id$
     3.6      Author:     Norbert Schirmer, Tobias Nipkow, Martin Wildmoser
     3.7  *)
     3.8  
     3.9  header {* Map operations implemented on association lists*}
    3.10  
    3.11  theory AssocList 
    3.12 -imports Plain "~~/src/HOL/Map"
    3.13 +imports Map Main
    3.14  begin
    3.15  
    3.16  text {*
     4.1 --- a/src/HOL/Library/Binomial.thy	Mon Mar 23 07:41:07 2009 +0100
     4.2 +++ b/src/HOL/Library/Binomial.thy	Mon Mar 23 08:16:24 2009 +0100
     4.3 @@ -6,7 +6,7 @@
     4.4  header {* Binomial Coefficients *}
     4.5  
     4.6  theory Binomial
     4.7 -imports Fact Plain "~~/src/HOL/SetInterval" Presburger 
     4.8 +imports Fact SetInterval Presburger Main
     4.9  begin
    4.10  
    4.11  text {* This development is based on the work of Andy Gordon and
     5.1 --- a/src/HOL/Library/Boolean_Algebra.thy	Mon Mar 23 07:41:07 2009 +0100
     5.2 +++ b/src/HOL/Library/Boolean_Algebra.thy	Mon Mar 23 08:16:24 2009 +0100
     5.3 @@ -5,7 +5,7 @@
     5.4  header {* Boolean Algebras *}
     5.5  
     5.6  theory Boolean_Algebra
     5.7 -imports Plain
     5.8 +imports Main
     5.9  begin
    5.10  
    5.11  locale boolean =
     6.1 --- a/src/HOL/Library/Char_nat.thy	Mon Mar 23 07:41:07 2009 +0100
     6.2 +++ b/src/HOL/Library/Char_nat.thy	Mon Mar 23 08:16:24 2009 +0100
     6.3 @@ -1,12 +1,11 @@
     6.4  (*  Title:      HOL/Library/Char_nat.thy
     6.5 -    ID:         $Id$
     6.6      Author:     Norbert Voelker, Florian Haftmann
     6.7  *)
     6.8  
     6.9  header {* Mapping between characters and natural numbers *}
    6.10  
    6.11  theory Char_nat
    6.12 -imports Plain "~~/src/HOL/List"
    6.13 +imports List Main
    6.14  begin
    6.15  
    6.16  text {* Conversions between nibbles and natural numbers in [0..15]. *}
     7.1 --- a/src/HOL/Library/Char_ord.thy	Mon Mar 23 07:41:07 2009 +0100
     7.2 +++ b/src/HOL/Library/Char_ord.thy	Mon Mar 23 08:16:24 2009 +0100
     7.3 @@ -1,12 +1,11 @@
     7.4  (*  Title:      HOL/Library/Char_ord.thy
     7.5 -    ID:         $Id$
     7.6      Author:     Norbert Voelker, Florian Haftmann
     7.7  *)
     7.8  
     7.9  header {* Order on characters *}
    7.10  
    7.11  theory Char_ord
    7.12 -imports Plain Product_ord Char_nat
    7.13 +imports Product_ord Char_nat Main
    7.14  begin
    7.15  
    7.16  instantiation nibble :: linorder
     8.1 --- a/src/HOL/Library/Code_Char.thy	Mon Mar 23 07:41:07 2009 +0100
     8.2 +++ b/src/HOL/Library/Code_Char.thy	Mon Mar 23 08:16:24 2009 +0100
     8.3 @@ -5,7 +5,7 @@
     8.4  header {* Code generation of pretty characters (and strings) *}
     8.5  
     8.6  theory Code_Char
     8.7 -imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Eval"
     8.8 +imports List Code_Eval Main
     8.9  begin
    8.10  
    8.11  code_type char
     9.1 --- a/src/HOL/Library/Code_Char_chr.thy	Mon Mar 23 07:41:07 2009 +0100
     9.2 +++ b/src/HOL/Library/Code_Char_chr.thy	Mon Mar 23 08:16:24 2009 +0100
     9.3 @@ -1,12 +1,11 @@
     9.4  (*  Title:      HOL/Library/Code_Char_chr.thy
     9.5 -    ID:         $Id$
     9.6      Author:     Florian Haftmann
     9.7  *)
     9.8  
     9.9  header {* Code generation of pretty characters with character codes *}
    9.10  
    9.11  theory Code_Char_chr
    9.12 -imports Plain Char_nat Code_Char Code_Integer
    9.13 +imports Char_nat Code_Char Code_Integer Main
    9.14  begin
    9.15  
    9.16  definition
    10.1 --- a/src/HOL/Library/Code_Index.thy	Mon Mar 23 07:41:07 2009 +0100
    10.2 +++ b/src/HOL/Library/Code_Index.thy	Mon Mar 23 08:16:24 2009 +0100
    10.3 @@ -3,7 +3,7 @@
    10.4  header {* Type of indices *}
    10.5  
    10.6  theory Code_Index
    10.7 -imports Plain "~~/src/HOL/Code_Eval" "~~/src/HOL/Presburger"
    10.8 +imports Main
    10.9  begin
   10.10  
   10.11  text {*
    11.1 --- a/src/HOL/Library/Code_Integer.thy	Mon Mar 23 07:41:07 2009 +0100
    11.2 +++ b/src/HOL/Library/Code_Integer.thy	Mon Mar 23 08:16:24 2009 +0100
    11.3 @@ -5,7 +5,7 @@
    11.4  header {* Pretty integer literals for code generation *}
    11.5  
    11.6  theory Code_Integer
    11.7 -imports Plain "~~/src/HOL/Code_Eval" "~~/src/HOL/Presburger"
    11.8 +imports Main
    11.9  begin
   11.10  
   11.11  text {*
    12.1 --- a/src/HOL/Library/Coinductive_List.thy	Mon Mar 23 07:41:07 2009 +0100
    12.2 +++ b/src/HOL/Library/Coinductive_List.thy	Mon Mar 23 08:16:24 2009 +0100
    12.3 @@ -1,12 +1,11 @@
    12.4  (*  Title:      HOL/Library/Coinductive_Lists.thy
    12.5 -    ID:         $Id$
    12.6      Author:     Lawrence C Paulson and Makarius
    12.7  *)
    12.8  
    12.9  header {* Potentially infinite lists as greatest fixed-point *}
   12.10  
   12.11  theory Coinductive_List
   12.12 -imports Plain "~~/src/HOL/List"
   12.13 +imports List Main
   12.14  begin
   12.15  
   12.16  subsection {* List constructors over the datatype universe *}
    13.1 --- a/src/HOL/Library/Commutative_Ring.thy	Mon Mar 23 07:41:07 2009 +0100
    13.2 +++ b/src/HOL/Library/Commutative_Ring.thy	Mon Mar 23 08:16:24 2009 +0100
    13.3 @@ -6,7 +6,7 @@
    13.4  header {* Proving equalities in commutative rings *}
    13.5  
    13.6  theory Commutative_Ring
    13.7 -imports Plain "~~/src/HOL/List" "~~/src/HOL/Parity"
    13.8 +imports List Parity Main
    13.9  uses ("comm_ring.ML")
   13.10  begin
   13.11  
    14.1 --- a/src/HOL/Library/ContNotDenum.thy	Mon Mar 23 07:41:07 2009 +0100
    14.2 +++ b/src/HOL/Library/ContNotDenum.thy	Mon Mar 23 08:16:24 2009 +0100
    14.3 @@ -5,7 +5,7 @@
    14.4  header {* Non-denumerability of the Continuum. *}
    14.5  
    14.6  theory ContNotDenum
    14.7 -imports RComplete Hilbert_Choice
    14.8 +imports Complex_Main
    14.9  begin
   14.10  
   14.11  subsection {* Abstract *}
    15.1 --- a/src/HOL/Library/Continuity.thy	Mon Mar 23 07:41:07 2009 +0100
    15.2 +++ b/src/HOL/Library/Continuity.thy	Mon Mar 23 08:16:24 2009 +0100
    15.3 @@ -1,12 +1,11 @@
    15.4  (*  Title:      HOL/Library/Continuity.thy
    15.5 -    ID:         $Id$
    15.6      Author:     David von Oheimb, TU Muenchen
    15.7  *)
    15.8  
    15.9  header {* Continuity and iterations (of set transformers) *}
   15.10  
   15.11  theory Continuity
   15.12 -imports Plain "~~/src/HOL/Relation_Power"
   15.13 +imports Relation_Power Main
   15.14  begin
   15.15  
   15.16  subsection {* Continuity for complete lattices *}
    16.1 --- a/src/HOL/Library/Countable.thy	Mon Mar 23 07:41:07 2009 +0100
    16.2 +++ b/src/HOL/Library/Countable.thy	Mon Mar 23 08:16:24 2009 +0100
    16.3 @@ -6,11 +6,11 @@
    16.4  
    16.5  theory Countable
    16.6  imports
    16.7 -  Plain
    16.8    "~~/src/HOL/List"
    16.9    "~~/src/HOL/Hilbert_Choice"
   16.10    "~~/src/HOL/Nat_Int_Bij"
   16.11    "~~/src/HOL/Rational"
   16.12 +  Main
   16.13  begin
   16.14  
   16.15  subsection {* The class of countable types *}
    17.1 --- a/src/HOL/Library/Determinants.thy	Mon Mar 23 07:41:07 2009 +0100
    17.2 +++ b/src/HOL/Library/Determinants.thy	Mon Mar 23 08:16:24 2009 +0100
    17.3 @@ -5,7 +5,7 @@
    17.4  header {* Traces, Determinant of square matrices and some properties *}
    17.5  
    17.6  theory Determinants
    17.7 -  imports Euclidean_Space Permutations
    17.8 +imports Euclidean_Space Permutations
    17.9  begin
   17.10  
   17.11  subsection{* First some facts about products*}
    18.1 --- a/src/HOL/Library/Efficient_Nat.thy	Mon Mar 23 07:41:07 2009 +0100
    18.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Mon Mar 23 08:16:24 2009 +0100
    18.3 @@ -5,7 +5,7 @@
    18.4  header {* Implementation of natural numbers by target-language integers *}
    18.5  
    18.6  theory Efficient_Nat
    18.7 -imports Code_Index Code_Integer
    18.8 +imports Code_Index Code_Integer Main
    18.9  begin
   18.10  
   18.11  text {*
    19.1 --- a/src/HOL/Library/Enum.thy	Mon Mar 23 07:41:07 2009 +0100
    19.2 +++ b/src/HOL/Library/Enum.thy	Mon Mar 23 08:16:24 2009 +0100
    19.3 @@ -5,7 +5,7 @@
    19.4  header {* Finite types as explicit enumerations *}
    19.5  
    19.6  theory Enum
    19.7 -imports Plain "~~/src/HOL/Map"
    19.8 +imports Map Main
    19.9  begin
   19.10  
   19.11  subsection {* Class @{text enum} *}
    20.1 --- a/src/HOL/Library/Euclidean_Space.thy	Mon Mar 23 07:41:07 2009 +0100
    20.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Mon Mar 23 08:16:24 2009 +0100
    20.3 @@ -5,7 +5,8 @@
    20.4  header {* (Real) Vectors in Euclidean space, and elementary linear algebra.*}
    20.5  
    20.6  theory Euclidean_Space
    20.7 -imports Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
    20.8 +imports
    20.9 +  Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
   20.10    Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type
   20.11    Inner_Product
   20.12  uses ("normarith.ML")
    21.1 --- a/src/HOL/Library/Eval_Witness.thy	Mon Mar 23 07:41:07 2009 +0100
    21.2 +++ b/src/HOL/Library/Eval_Witness.thy	Mon Mar 23 08:16:24 2009 +0100
    21.3 @@ -5,7 +5,7 @@
    21.4  header {* Evaluation Oracle with ML witnesses *}
    21.5  
    21.6  theory Eval_Witness
    21.7 -imports Plain "~~/src/HOL/List"
    21.8 +imports List Main
    21.9  begin
   21.10  
   21.11  text {* 
    22.1 --- a/src/HOL/Library/Executable_Set.thy	Mon Mar 23 07:41:07 2009 +0100
    22.2 +++ b/src/HOL/Library/Executable_Set.thy	Mon Mar 23 08:16:24 2009 +0100
    22.3 @@ -1,12 +1,11 @@
    22.4  (*  Title:      HOL/Library/Executable_Set.thy
    22.5 -    ID:         $Id$
    22.6      Author:     Stefan Berghofer, TU Muenchen
    22.7  *)
    22.8  
    22.9  header {* Implementation of finite sets by lists *}
   22.10  
   22.11  theory Executable_Set
   22.12 -imports Plain "~~/src/HOL/List"
   22.13 +imports Main
   22.14  begin
   22.15  
   22.16  subsection {* Definitional rewrites *}
    23.1 --- a/src/HOL/Library/Finite_Cartesian_Product.thy	Mon Mar 23 07:41:07 2009 +0100
    23.2 +++ b/src/HOL/Library/Finite_Cartesian_Product.thy	Mon Mar 23 08:16:24 2009 +0100
    23.3 @@ -5,12 +5,9 @@
    23.4  header {* Definition of finite Cartesian product types. *}
    23.5  
    23.6  theory Finite_Cartesian_Product
    23.7 -  (* imports Plain SetInterval ATP_Linkup *)
    23.8 -imports Main
    23.9 +imports Main (*FIXME: ATP_Linkup is only needed for metis at a few places. We could dispense of that by changing the proofs.*)
   23.10  begin
   23.11  
   23.12 -  (* FIXME : ATP_Linkup is only needed for metis at a few places. We could dispense of that by changing the proofs*)
   23.13 -
   23.14  definition hassize (infixr "hassize" 12) where
   23.15    "(S hassize n) = (finite S \<and> card S = n)"
   23.16  
    24.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Mon Mar 23 07:41:07 2009 +0100
    24.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Mon Mar 23 08:16:24 2009 +0100
    24.3 @@ -1,12 +1,11 @@
    24.4  (*  Title:      Formal_Power_Series.thy
    24.5 -    ID:
    24.6      Author:     Amine Chaieb, University of Cambridge
    24.7  *)
    24.8  
    24.9  header{* A formalization of formal power series *}
   24.10  
   24.11  theory Formal_Power_Series
   24.12 -  imports Main Fact Parity
   24.13 +imports Main Fact Parity
   24.14  begin
   24.15  
   24.16  subsection {* The type of formal power series*}
    25.1 --- a/src/HOL/Library/FrechetDeriv.thy	Mon Mar 23 07:41:07 2009 +0100
    25.2 +++ b/src/HOL/Library/FrechetDeriv.thy	Mon Mar 23 08:16:24 2009 +0100
    25.3 @@ -1,12 +1,11 @@
    25.4  (*  Title       : FrechetDeriv.thy
    25.5 -    ID          : $Id$
    25.6      Author      : Brian Huffman
    25.7  *)
    25.8  
    25.9  header {* Frechet Derivative *}
   25.10  
   25.11  theory FrechetDeriv
   25.12 -imports Lim
   25.13 +imports Lim Complex_Main
   25.14  begin
   25.15  
   25.16  definition
    26.1 --- a/src/HOL/Library/FuncSet.thy	Mon Mar 23 07:41:07 2009 +0100
    26.2 +++ b/src/HOL/Library/FuncSet.thy	Mon Mar 23 08:16:24 2009 +0100
    26.3 @@ -1,12 +1,11 @@
    26.4  (*  Title:      HOL/Library/FuncSet.thy
    26.5 -    ID:         $Id$
    26.6      Author:     Florian Kammueller and Lawrence C Paulson
    26.7  *)
    26.8  
    26.9  header {* Pi and Function Sets *}
   26.10  
   26.11  theory FuncSet
   26.12 -imports Plain "~~/src/HOL/Hilbert_Choice"
   26.13 +imports Hilbert_Choice Main
   26.14  begin
   26.15  
   26.16  definition
    27.1 --- a/src/HOL/Library/Glbs.thy	Mon Mar 23 07:41:07 2009 +0100
    27.2 +++ b/src/HOL/Library/Glbs.thy	Mon Mar 23 08:16:24 2009 +0100
    27.3 @@ -1,8 +1,6 @@
    27.4 -(* Title:      Glbs
    27.5 -   Author:     Amine Chaieb, University of Cambridge
    27.6 -*)
    27.7 +(* Author: Amine Chaieb, University of Cambridge *)
    27.8  
    27.9 -header{*Definitions of Lower Bounds and Greatest Lower Bounds, analogous to Lubs*}
   27.10 +header {* Definitions of Lower Bounds and Greatest Lower Bounds, analogous to Lubs *}
   27.11  
   27.12  theory Glbs
   27.13  imports Lubs
    28.1 --- a/src/HOL/Library/Infinite_Set.thy	Mon Mar 23 07:41:07 2009 +0100
    28.2 +++ b/src/HOL/Library/Infinite_Set.thy	Mon Mar 23 08:16:24 2009 +0100
    28.3 @@ -1,15 +1,13 @@
    28.4  (*  Title:      HOL/Library/Infinite_Set.thy
    28.5 -    ID:         $Id$
    28.6      Author:     Stephan Merz
    28.7  *)
    28.8  
    28.9  header {* Infinite Sets and Related Concepts *}
   28.10  
   28.11  theory Infinite_Set
   28.12 -imports Main "~~/src/HOL/SetInterval" "~~/src/HOL/Hilbert_Choice"
   28.13 +imports Main
   28.14  begin
   28.15  
   28.16 -
   28.17  subsection "Infinite Sets"
   28.18  
   28.19  text {*
    29.1 --- a/src/HOL/Library/Inner_Product.thy	Mon Mar 23 07:41:07 2009 +0100
    29.2 +++ b/src/HOL/Library/Inner_Product.thy	Mon Mar 23 08:16:24 2009 +0100
    29.3 @@ -5,7 +5,7 @@
    29.4  header {* Inner Product Spaces and the Gradient Derivative *}
    29.5  
    29.6  theory Inner_Product
    29.7 -imports Complex FrechetDeriv
    29.8 +imports Complex_Main FrechetDeriv
    29.9  begin
   29.10  
   29.11  subsection {* Real inner product spaces *}
    30.1 --- a/src/HOL/Library/LaTeXsugar.thy	Mon Mar 23 07:41:07 2009 +0100
    30.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Mon Mar 23 08:16:24 2009 +0100
    30.3 @@ -5,7 +5,7 @@
    30.4  
    30.5  (*<*)
    30.6  theory LaTeXsugar
    30.7 -imports Plain "~~/src/HOL/List"
    30.8 +imports Main
    30.9  begin
   30.10  
   30.11  (* LOGIC *)
    31.1 --- a/src/HOL/Library/ListVector.thy	Mon Mar 23 07:41:07 2009 +0100
    31.2 +++ b/src/HOL/Library/ListVector.thy	Mon Mar 23 08:16:24 2009 +0100
    31.3 @@ -1,11 +1,9 @@
    31.4 -(*  ID:         $Id$
    31.5 -    Author:     Tobias Nipkow, 2007
    31.6 -*)
    31.7 +(*  Author: Tobias Nipkow, 2007 *)
    31.8  
    31.9 -header "Lists as vectors"
   31.10 +header {* Lists as vectors *}
   31.11  
   31.12  theory ListVector
   31.13 -imports Plain "~~/src/HOL/List"
   31.14 +imports List Main
   31.15  begin
   31.16  
   31.17  text{* \noindent
    32.1 --- a/src/HOL/Library/List_Prefix.thy	Mon Mar 23 07:41:07 2009 +0100
    32.2 +++ b/src/HOL/Library/List_Prefix.thy	Mon Mar 23 08:16:24 2009 +0100
    32.3 @@ -1,12 +1,11 @@
    32.4  (*  Title:      HOL/Library/List_Prefix.thy
    32.5 -    ID:         $Id$
    32.6      Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
    32.7  *)
    32.8  
    32.9  header {* List prefixes and postfixes *}
   32.10  
   32.11  theory List_Prefix
   32.12 -imports Plain "~~/src/HOL/List"
   32.13 +imports List Main
   32.14  begin
   32.15  
   32.16  subsection {* Prefix order on lists *}
    33.1 --- a/src/HOL/Library/List_lexord.thy	Mon Mar 23 07:41:07 2009 +0100
    33.2 +++ b/src/HOL/Library/List_lexord.thy	Mon Mar 23 08:16:24 2009 +0100
    33.3 @@ -1,12 +1,11 @@
    33.4  (*  Title:      HOL/Library/List_lexord.thy
    33.5 -    ID:         $Id$
    33.6      Author:     Norbert Voelker
    33.7  *)
    33.8  
    33.9  header {* Lexicographic order on lists *}
   33.10  
   33.11  theory List_lexord
   33.12 -imports Plain "~~/src/HOL/List"
   33.13 +imports List Main
   33.14  begin
   33.15  
   33.16  instantiation list :: (ord) ord
    34.1 --- a/src/HOL/Library/Mapping.thy	Mon Mar 23 07:41:07 2009 +0100
    34.2 +++ b/src/HOL/Library/Mapping.thy	Mon Mar 23 08:16:24 2009 +0100
    34.3 @@ -5,7 +5,7 @@
    34.4  header {* An abstract view on maps for code generation. *}
    34.5  
    34.6  theory Mapping
    34.7 -imports Map
    34.8 +imports Map Main
    34.9  begin
   34.10  
   34.11  subsection {* Type definition and primitive operations *}
    35.1 --- a/src/HOL/Library/Multiset.thy	Mon Mar 23 07:41:07 2009 +0100
    35.2 +++ b/src/HOL/Library/Multiset.thy	Mon Mar 23 08:16:24 2009 +0100
    35.3 @@ -5,7 +5,7 @@
    35.4  header {* Multisets *}
    35.5  
    35.6  theory Multiset
    35.7 -imports Plain "~~/src/HOL/List"
    35.8 +imports List Main
    35.9  begin
   35.10  
   35.11  subsection {* The type of multisets *}
    36.1 --- a/src/HOL/Library/Nat_Infinity.thy	Mon Mar 23 07:41:07 2009 +0100
    36.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Mon Mar 23 08:16:24 2009 +0100
    36.3 @@ -5,7 +5,7 @@
    36.4  header {* Natural numbers with infinity *}
    36.5  
    36.6  theory Nat_Infinity
    36.7 -imports Plain "~~/src/HOL/Presburger"
    36.8 +imports Main
    36.9  begin
   36.10  
   36.11  subsection {* Type definition *}
    37.1 --- a/src/HOL/Library/Nat_Int_Bij.thy	Mon Mar 23 07:41:07 2009 +0100
    37.2 +++ b/src/HOL/Library/Nat_Int_Bij.thy	Mon Mar 23 08:16:24 2009 +0100
    37.3 @@ -1,12 +1,11 @@
    37.4  (*  Title:      HOL/Nat_Int_Bij.thy
    37.5 -    ID:         $Id$
    37.6      Author:     Stefan Richter, Tobias Nipkow
    37.7  *)
    37.8  
    37.9  header{* Bijections $\mathbb{N}\to\mathbb{N}^2$ and $\mathbb{N}\to\mathbb{Z}$*}
   37.10  
   37.11  theory Nat_Int_Bij
   37.12 -imports Hilbert_Choice Presburger
   37.13 +imports Main
   37.14  begin
   37.15  
   37.16  subsection{*  A bijection between @{text "\<nat>"} and @{text "\<nat>\<twosuperior>"} *}
    38.1 --- a/src/HOL/Library/Nested_Environment.thy	Mon Mar 23 07:41:07 2009 +0100
    38.2 +++ b/src/HOL/Library/Nested_Environment.thy	Mon Mar 23 08:16:24 2009 +0100
    38.3 @@ -1,12 +1,11 @@
    38.4  (*  Title:      HOL/Library/Nested_Environment.thy
    38.5 -    ID:         $Id$
    38.6      Author:     Markus Wenzel, TU Muenchen
    38.7  *)
    38.8  
    38.9  header {* Nested environments *}
   38.10  
   38.11  theory Nested_Environment
   38.12 -imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Eval"
   38.13 +imports Main
   38.14  begin
   38.15  
   38.16  text {*
    39.1 --- a/src/HOL/Library/Numeral_Type.thy	Mon Mar 23 07:41:07 2009 +0100
    39.2 +++ b/src/HOL/Library/Numeral_Type.thy	Mon Mar 23 08:16:24 2009 +0100
    39.3 @@ -5,7 +5,7 @@
    39.4  header {* Numeral Syntax for Types *}
    39.5  
    39.6  theory Numeral_Type
    39.7 -imports Plain "~~/src/HOL/Presburger"
    39.8 +imports Main
    39.9  begin
   39.10  
   39.11  subsection {* Preliminary lemmas *}
    40.1 --- a/src/HOL/Library/Option_ord.thy	Mon Mar 23 07:41:07 2009 +0100
    40.2 +++ b/src/HOL/Library/Option_ord.thy	Mon Mar 23 08:16:24 2009 +0100
    40.3 @@ -1,15 +1,14 @@
    40.4  (*  Title:      HOL/Library/Option_ord.thy
    40.5 -    ID:         $Id$
    40.6      Author:     Florian Haftmann, TU Muenchen
    40.7  *)
    40.8  
    40.9  header {* Canonical order on option type *}
   40.10  
   40.11  theory Option_ord
   40.12 -imports Plain
   40.13 +imports Option Main
   40.14  begin
   40.15  
   40.16 -instantiation option :: (order) order
   40.17 +instantiation option :: (preorder) preorder
   40.18  begin
   40.19  
   40.20  definition less_eq_option where
   40.21 @@ -48,12 +47,63 @@
   40.22  lemma less_option_Some [simp, code]: "Some x < Some y \<longleftrightarrow> x < y"
   40.23    by (simp add: less_option_def)
   40.24  
   40.25 -instance by default
   40.26 -  (auto simp add: less_eq_option_def less_option_def split: option.splits)
   40.27 +instance proof
   40.28 +qed (auto simp add: less_eq_option_def less_option_def less_le_not_le elim: order_trans split: option.splits)
   40.29  
   40.30  end 
   40.31  
   40.32 -instance option :: (linorder) linorder
   40.33 -  by default (auto simp add: less_eq_option_def less_option_def split: option.splits)
   40.34 +instance option :: (order) order proof
   40.35 +qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
   40.36 +
   40.37 +instance option :: (linorder) linorder proof
   40.38 +qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
   40.39 +
   40.40 +instantiation option :: (preorder) bot
   40.41 +begin
   40.42 +
   40.43 +definition "bot = None"
   40.44 +
   40.45 +instance proof
   40.46 +qed (simp add: bot_option_def)
   40.47 +
   40.48 +end
   40.49 +
   40.50 +instantiation option :: (top) top
   40.51 +begin
   40.52 +
   40.53 +definition "top = Some top"
   40.54 +
   40.55 +instance proof
   40.56 +qed (simp add: top_option_def less_eq_option_def split: option.split)
   40.57  
   40.58  end
   40.59 +
   40.60 +instance option :: (wellorder) wellorder proof
   40.61 +  fix P :: "'a option \<Rightarrow> bool" and z :: "'a option"
   40.62 +  assume H: "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
   40.63 +  have "P None" by (rule H) simp
   40.64 +  then have P_Some [case_names Some]:
   40.65 +    "\<And>z. (\<And>x. z = Some x \<Longrightarrow> (P o Some) x) \<Longrightarrow> P z"
   40.66 +  proof -
   40.67 +    fix z
   40.68 +    assume "\<And>x. z = Some x \<Longrightarrow> (P o Some) x"
   40.69 +    with `P None` show "P z" by (cases z) simp_all
   40.70 +  qed
   40.71 +  show "P z" proof (cases z rule: P_Some)
   40.72 +    case (Some w)
   40.73 +    show "(P o Some) w" proof (induct rule: less_induct)
   40.74 +      case (less x)
   40.75 +      have "P (Some x)" proof (rule H)
   40.76 +        fix y :: "'a option"
   40.77 +        assume "y < Some x"
   40.78 +        show "P y" proof (cases y rule: P_Some)
   40.79 +          case (Some v) with `y < Some x` have "v < x" by simp
   40.80 +          with less show "(P o Some) v" .
   40.81 +        qed
   40.82 +      qed
   40.83 +      then show ?case by simp
   40.84 +    qed
   40.85 +  qed
   40.86 +qed
   40.87 +
   40.88 +end
    41.1 --- a/src/HOL/Library/OptionalSugar.thy	Mon Mar 23 07:41:07 2009 +0100
    41.2 +++ b/src/HOL/Library/OptionalSugar.thy	Mon Mar 23 08:16:24 2009 +0100
    41.3 @@ -4,7 +4,7 @@
    41.4  *)
    41.5  (*<*)
    41.6  theory OptionalSugar
    41.7 -imports LaTeXsugar Complex_Main
    41.8 +imports Complex_Main LaTeXsugar
    41.9  begin
   41.10  
   41.11  (* hiding set *)
    42.1 --- a/src/HOL/Library/Order_Relation.thy	Mon Mar 23 07:41:07 2009 +0100
    42.2 +++ b/src/HOL/Library/Order_Relation.thy	Mon Mar 23 08:16:24 2009 +0100
    42.3 @@ -1,6 +1,4 @@
    42.4 -(*  ID          : $Id$
    42.5 -    Author      : Tobias Nipkow
    42.6 -*)
    42.7 +(* Author: Tobias Nipkow *)
    42.8  
    42.9  header {* Orders as Relations *}
   42.10  
    43.1 --- a/src/HOL/Library/Permutations.thy	Mon Mar 23 07:41:07 2009 +0100
    43.2 +++ b/src/HOL/Library/Permutations.thy	Mon Mar 23 08:16:24 2009 +0100
    43.3 @@ -5,7 +5,7 @@
    43.4  header {* Permutations, both general and specifically on finite sets.*}
    43.5  
    43.6  theory Permutations
    43.7 -imports Main Finite_Cartesian_Product Parity Fact
    43.8 +imports Finite_Cartesian_Product Parity Fact Main
    43.9  begin
   43.10  
   43.11    (* Why should I import Main just to solve the Typerep problem! *)
    44.1 --- a/src/HOL/Library/Zorn.thy	Mon Mar 23 07:41:07 2009 +0100
    44.2 +++ b/src/HOL/Library/Zorn.thy	Mon Mar 23 08:16:24 2009 +0100
    44.3 @@ -7,7 +7,7 @@
    44.4  header {* Zorn's Lemma *}
    44.5  
    44.6  theory Zorn
    44.7 -imports "~~/src/HOL/Order_Relation"
    44.8 +imports Order_Relation Main
    44.9  begin
   44.10  
   44.11  (* Define globally? In Set.thy? *)
    45.1 --- a/src/HOL/ex/MergeSort.thy	Mon Mar 23 07:41:07 2009 +0100
    45.2 +++ b/src/HOL/ex/MergeSort.thy	Mon Mar 23 08:16:24 2009 +0100
    45.3 @@ -1,5 +1,4 @@
    45.4  (*  Title:      HOL/ex/Merge.thy
    45.5 -    ID:         $Id$
    45.6      Author:     Tobias Nipkow
    45.7      Copyright   2002 TU Muenchen
    45.8  *)