author haftmann Mon Mar 23 08:16:24 2009 +0100 (2009-03-23) changeset 30665 4cf38ea4fad2 parent 30659 a400b06d03cb parent 30664 167da873c3b3 child 30666 d6248d4508d5 child 30684 c98a64746c69 child 30734 ab05be086c4a
merged
     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.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.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.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.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.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