Main is (Complex_Main) base entry point in library theories
authorhaftmann
Mon Mar 23 08:14:24 2009 +0100 (2009-03-23)
changeset 306630b6aff7451b2
parent 30662 396be15b95d5
child 30664 167da873c3b3
Main is (Complex_Main) base entry point in library theories
src/HOL/Library/Abstract_Rat.thy
src/HOL/Library/AssocList.thy
src/HOL/Library/Binomial.thy
src/HOL/Library/Boolean_Algebra.thy
src/HOL/Library/Char_nat.thy
src/HOL/Library/Char_ord.thy
src/HOL/Library/Code_Char.thy
src/HOL/Library/Code_Char_chr.thy
src/HOL/Library/Code_Index.thy
src/HOL/Library/Code_Integer.thy
src/HOL/Library/Coinductive_List.thy
src/HOL/Library/Commutative_Ring.thy
src/HOL/Library/ContNotDenum.thy
src/HOL/Library/Continuity.thy
src/HOL/Library/Countable.thy
src/HOL/Library/Efficient_Nat.thy
src/HOL/Library/Enum.thy
src/HOL/Library/Eval_Witness.thy
src/HOL/Library/FrechetDeriv.thy
src/HOL/Library/FuncSet.thy
src/HOL/Library/Infinite_Set.thy
src/HOL/Library/Inner_Product.thy
src/HOL/Library/LaTeXsugar.thy
src/HOL/Library/ListVector.thy
src/HOL/Library/List_Prefix.thy
src/HOL/Library/List_lexord.thy
src/HOL/Library/Mapping.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Nat_Infinity.thy
src/HOL/Library/Nat_Int_Bij.thy
src/HOL/Library/Nested_Environment.thy
src/HOL/Library/Numeral_Type.thy
src/HOL/Library/OptionalSugar.thy
src/HOL/Library/Permutations.thy
src/HOL/Library/Zorn.thy
     1.1 --- a/src/HOL/Library/Abstract_Rat.thy	Mon Mar 23 08:14:23 2009 +0100
     1.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Mon Mar 23 08:14:24 2009 +0100
     1.3 @@ -1,12 +1,11 @@
     1.4  (*  Title:      HOL/Library/Abstract_Rat.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Amine Chaieb
     1.7  *)
     1.8  
     1.9  header {* Abstract rational numbers *}
    1.10  
    1.11  theory Abstract_Rat
    1.12 -imports Plain GCD
    1.13 +imports GCD Main
    1.14  begin
    1.15  
    1.16  types Num = "int \<times> int"
     2.1 --- a/src/HOL/Library/AssocList.thy	Mon Mar 23 08:14:23 2009 +0100
     2.2 +++ b/src/HOL/Library/AssocList.thy	Mon Mar 23 08:14:24 2009 +0100
     2.3 @@ -1,12 +1,11 @@
     2.4  (*  Title:      HOL/Library/AssocList.thy
     2.5 -    ID:         $Id$
     2.6      Author:     Norbert Schirmer, Tobias Nipkow, Martin Wildmoser
     2.7  *)
     2.8  
     2.9  header {* Map operations implemented on association lists*}
    2.10  
    2.11  theory AssocList 
    2.12 -imports Plain "~~/src/HOL/Map"
    2.13 +imports Map Main
    2.14  begin
    2.15  
    2.16  text {*
     3.1 --- a/src/HOL/Library/Binomial.thy	Mon Mar 23 08:14:23 2009 +0100
     3.2 +++ b/src/HOL/Library/Binomial.thy	Mon Mar 23 08:14:24 2009 +0100
     3.3 @@ -6,7 +6,7 @@
     3.4  header {* Binomial Coefficients *}
     3.5  
     3.6  theory Binomial
     3.7 -imports Fact Plain "~~/src/HOL/SetInterval" Presburger 
     3.8 +imports Fact SetInterval Presburger Main
     3.9  begin
    3.10  
    3.11  text {* This development is based on the work of Andy Gordon and
     4.1 --- a/src/HOL/Library/Boolean_Algebra.thy	Mon Mar 23 08:14:23 2009 +0100
     4.2 +++ b/src/HOL/Library/Boolean_Algebra.thy	Mon Mar 23 08:14:24 2009 +0100
     4.3 @@ -5,7 +5,7 @@
     4.4  header {* Boolean Algebras *}
     4.5  
     4.6  theory Boolean_Algebra
     4.7 -imports Plain
     4.8 +imports Main
     4.9  begin
    4.10  
    4.11  locale boolean =
     5.1 --- a/src/HOL/Library/Char_nat.thy	Mon Mar 23 08:14:23 2009 +0100
     5.2 +++ b/src/HOL/Library/Char_nat.thy	Mon Mar 23 08:14:24 2009 +0100
     5.3 @@ -1,12 +1,11 @@
     5.4  (*  Title:      HOL/Library/Char_nat.thy
     5.5 -    ID:         $Id$
     5.6      Author:     Norbert Voelker, Florian Haftmann
     5.7  *)
     5.8  
     5.9  header {* Mapping between characters and natural numbers *}
    5.10  
    5.11  theory Char_nat
    5.12 -imports Plain "~~/src/HOL/List"
    5.13 +imports List Main
    5.14  begin
    5.15  
    5.16  text {* Conversions between nibbles and natural numbers in [0..15]. *}
     6.1 --- a/src/HOL/Library/Char_ord.thy	Mon Mar 23 08:14:23 2009 +0100
     6.2 +++ b/src/HOL/Library/Char_ord.thy	Mon Mar 23 08:14:24 2009 +0100
     6.3 @@ -1,12 +1,11 @@
     6.4  (*  Title:      HOL/Library/Char_ord.thy
     6.5 -    ID:         $Id$
     6.6      Author:     Norbert Voelker, Florian Haftmann
     6.7  *)
     6.8  
     6.9  header {* Order on characters *}
    6.10  
    6.11  theory Char_ord
    6.12 -imports Plain Product_ord Char_nat
    6.13 +imports Product_ord Char_nat Main
    6.14  begin
    6.15  
    6.16  instantiation nibble :: linorder
     7.1 --- a/src/HOL/Library/Code_Char.thy	Mon Mar 23 08:14:23 2009 +0100
     7.2 +++ b/src/HOL/Library/Code_Char.thy	Mon Mar 23 08:14:24 2009 +0100
     7.3 @@ -5,7 +5,7 @@
     7.4  header {* Code generation of pretty characters (and strings) *}
     7.5  
     7.6  theory Code_Char
     7.7 -imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Eval"
     7.8 +imports List Code_Eval Main
     7.9  begin
    7.10  
    7.11  code_type char
     8.1 --- a/src/HOL/Library/Code_Char_chr.thy	Mon Mar 23 08:14:23 2009 +0100
     8.2 +++ b/src/HOL/Library/Code_Char_chr.thy	Mon Mar 23 08:14:24 2009 +0100
     8.3 @@ -1,12 +1,11 @@
     8.4  (*  Title:      HOL/Library/Code_Char_chr.thy
     8.5 -    ID:         $Id$
     8.6      Author:     Florian Haftmann
     8.7  *)
     8.8  
     8.9  header {* Code generation of pretty characters with character codes *}
    8.10  
    8.11  theory Code_Char_chr
    8.12 -imports Plain Char_nat Code_Char Code_Integer
    8.13 +imports Char_nat Code_Char Code_Integer Main
    8.14  begin
    8.15  
    8.16  definition
     9.1 --- a/src/HOL/Library/Code_Index.thy	Mon Mar 23 08:14:23 2009 +0100
     9.2 +++ b/src/HOL/Library/Code_Index.thy	Mon Mar 23 08:14:24 2009 +0100
     9.3 @@ -3,7 +3,7 @@
     9.4  header {* Type of indices *}
     9.5  
     9.6  theory Code_Index
     9.7 -imports Plain "~~/src/HOL/Code_Eval" "~~/src/HOL/Presburger"
     9.8 +imports Main
     9.9  begin
    9.10  
    9.11  text {*
    10.1 --- a/src/HOL/Library/Code_Integer.thy	Mon Mar 23 08:14:23 2009 +0100
    10.2 +++ b/src/HOL/Library/Code_Integer.thy	Mon Mar 23 08:14:24 2009 +0100
    10.3 @@ -5,7 +5,7 @@
    10.4  header {* Pretty integer literals for code generation *}
    10.5  
    10.6  theory Code_Integer
    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/Coinductive_List.thy	Mon Mar 23 08:14:23 2009 +0100
    11.2 +++ b/src/HOL/Library/Coinductive_List.thy	Mon Mar 23 08:14:24 2009 +0100
    11.3 @@ -1,12 +1,11 @@
    11.4  (*  Title:      HOL/Library/Coinductive_Lists.thy
    11.5 -    ID:         $Id$
    11.6      Author:     Lawrence C Paulson and Makarius
    11.7  *)
    11.8  
    11.9  header {* Potentially infinite lists as greatest fixed-point *}
   11.10  
   11.11  theory Coinductive_List
   11.12 -imports Plain "~~/src/HOL/List"
   11.13 +imports List Main
   11.14  begin
   11.15  
   11.16  subsection {* List constructors over the datatype universe *}
    12.1 --- a/src/HOL/Library/Commutative_Ring.thy	Mon Mar 23 08:14:23 2009 +0100
    12.2 +++ b/src/HOL/Library/Commutative_Ring.thy	Mon Mar 23 08:14:24 2009 +0100
    12.3 @@ -6,7 +6,7 @@
    12.4  header {* Proving equalities in commutative rings *}
    12.5  
    12.6  theory Commutative_Ring
    12.7 -imports Plain "~~/src/HOL/List" "~~/src/HOL/Parity"
    12.8 +imports List Parity Main
    12.9  uses ("comm_ring.ML")
   12.10  begin
   12.11  
    13.1 --- a/src/HOL/Library/ContNotDenum.thy	Mon Mar 23 08:14:23 2009 +0100
    13.2 +++ b/src/HOL/Library/ContNotDenum.thy	Mon Mar 23 08:14:24 2009 +0100
    13.3 @@ -5,7 +5,7 @@
    13.4  header {* Non-denumerability of the Continuum. *}
    13.5  
    13.6  theory ContNotDenum
    13.7 -imports RComplete Hilbert_Choice
    13.8 +imports Complex_Main
    13.9  begin
   13.10  
   13.11  subsection {* Abstract *}
    14.1 --- a/src/HOL/Library/Continuity.thy	Mon Mar 23 08:14:23 2009 +0100
    14.2 +++ b/src/HOL/Library/Continuity.thy	Mon Mar 23 08:14:24 2009 +0100
    14.3 @@ -1,12 +1,11 @@
    14.4  (*  Title:      HOL/Library/Continuity.thy
    14.5 -    ID:         $Id$
    14.6      Author:     David von Oheimb, TU Muenchen
    14.7  *)
    14.8  
    14.9  header {* Continuity and iterations (of set transformers) *}
   14.10  
   14.11  theory Continuity
   14.12 -imports Plain "~~/src/HOL/Relation_Power"
   14.13 +imports Relation_Power Main
   14.14  begin
   14.15  
   14.16  subsection {* Continuity for complete lattices *}
    15.1 --- a/src/HOL/Library/Countable.thy	Mon Mar 23 08:14:23 2009 +0100
    15.2 +++ b/src/HOL/Library/Countable.thy	Mon Mar 23 08:14:24 2009 +0100
    15.3 @@ -6,11 +6,11 @@
    15.4  
    15.5  theory Countable
    15.6  imports
    15.7 -  Plain
    15.8    "~~/src/HOL/List"
    15.9    "~~/src/HOL/Hilbert_Choice"
   15.10    "~~/src/HOL/Nat_Int_Bij"
   15.11    "~~/src/HOL/Rational"
   15.12 +  Main
   15.13  begin
   15.14  
   15.15  subsection {* The class of countable types *}
    16.1 --- a/src/HOL/Library/Efficient_Nat.thy	Mon Mar 23 08:14:23 2009 +0100
    16.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Mon Mar 23 08:14:24 2009 +0100
    16.3 @@ -5,7 +5,7 @@
    16.4  header {* Implementation of natural numbers by target-language integers *}
    16.5  
    16.6  theory Efficient_Nat
    16.7 -imports Code_Index Code_Integer
    16.8 +imports Code_Index Code_Integer Main
    16.9  begin
   16.10  
   16.11  text {*
    17.1 --- a/src/HOL/Library/Enum.thy	Mon Mar 23 08:14:23 2009 +0100
    17.2 +++ b/src/HOL/Library/Enum.thy	Mon Mar 23 08:14:24 2009 +0100
    17.3 @@ -5,7 +5,7 @@
    17.4  header {* Finite types as explicit enumerations *}
    17.5  
    17.6  theory Enum
    17.7 -imports Plain "~~/src/HOL/Map"
    17.8 +imports Map Main
    17.9  begin
   17.10  
   17.11  subsection {* Class @{text enum} *}
    18.1 --- a/src/HOL/Library/Eval_Witness.thy	Mon Mar 23 08:14:23 2009 +0100
    18.2 +++ b/src/HOL/Library/Eval_Witness.thy	Mon Mar 23 08:14:24 2009 +0100
    18.3 @@ -5,7 +5,7 @@
    18.4  header {* Evaluation Oracle with ML witnesses *}
    18.5  
    18.6  theory Eval_Witness
    18.7 -imports Plain "~~/src/HOL/List"
    18.8 +imports List Main
    18.9  begin
   18.10  
   18.11  text {* 
    19.1 --- a/src/HOL/Library/FrechetDeriv.thy	Mon Mar 23 08:14:23 2009 +0100
    19.2 +++ b/src/HOL/Library/FrechetDeriv.thy	Mon Mar 23 08:14:24 2009 +0100
    19.3 @@ -1,12 +1,11 @@
    19.4  (*  Title       : FrechetDeriv.thy
    19.5 -    ID          : $Id$
    19.6      Author      : Brian Huffman
    19.7  *)
    19.8  
    19.9  header {* Frechet Derivative *}
   19.10  
   19.11  theory FrechetDeriv
   19.12 -imports Lim
   19.13 +imports Lim Complex_Main
   19.14  begin
   19.15  
   19.16  definition
    20.1 --- a/src/HOL/Library/FuncSet.thy	Mon Mar 23 08:14:23 2009 +0100
    20.2 +++ b/src/HOL/Library/FuncSet.thy	Mon Mar 23 08:14:24 2009 +0100
    20.3 @@ -1,12 +1,11 @@
    20.4  (*  Title:      HOL/Library/FuncSet.thy
    20.5 -    ID:         $Id$
    20.6      Author:     Florian Kammueller and Lawrence C Paulson
    20.7  *)
    20.8  
    20.9  header {* Pi and Function Sets *}
   20.10  
   20.11  theory FuncSet
   20.12 -imports Plain "~~/src/HOL/Hilbert_Choice"
   20.13 +imports Hilbert_Choice Main
   20.14  begin
   20.15  
   20.16  definition
    21.1 --- a/src/HOL/Library/Infinite_Set.thy	Mon Mar 23 08:14:23 2009 +0100
    21.2 +++ b/src/HOL/Library/Infinite_Set.thy	Mon Mar 23 08:14:24 2009 +0100
    21.3 @@ -1,15 +1,13 @@
    21.4  (*  Title:      HOL/Library/Infinite_Set.thy
    21.5 -    ID:         $Id$
    21.6      Author:     Stephan Merz
    21.7  *)
    21.8  
    21.9  header {* Infinite Sets and Related Concepts *}
   21.10  
   21.11  theory Infinite_Set
   21.12 -imports Main "~~/src/HOL/SetInterval" "~~/src/HOL/Hilbert_Choice"
   21.13 +imports Main
   21.14  begin
   21.15  
   21.16 -
   21.17  subsection "Infinite Sets"
   21.18  
   21.19  text {*
    22.1 --- a/src/HOL/Library/Inner_Product.thy	Mon Mar 23 08:14:23 2009 +0100
    22.2 +++ b/src/HOL/Library/Inner_Product.thy	Mon Mar 23 08:14:24 2009 +0100
    22.3 @@ -5,7 +5,7 @@
    22.4  header {* Inner Product Spaces and the Gradient Derivative *}
    22.5  
    22.6  theory Inner_Product
    22.7 -imports Complex FrechetDeriv
    22.8 +imports Complex_Main FrechetDeriv
    22.9  begin
   22.10  
   22.11  subsection {* Real inner product spaces *}
    23.1 --- a/src/HOL/Library/LaTeXsugar.thy	Mon Mar 23 08:14:23 2009 +0100
    23.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Mon Mar 23 08:14:24 2009 +0100
    23.3 @@ -5,7 +5,7 @@
    23.4  
    23.5  (*<*)
    23.6  theory LaTeXsugar
    23.7 -imports Plain "~~/src/HOL/List"
    23.8 +imports Main
    23.9  begin
   23.10  
   23.11  (* LOGIC *)
    24.1 --- a/src/HOL/Library/ListVector.thy	Mon Mar 23 08:14:23 2009 +0100
    24.2 +++ b/src/HOL/Library/ListVector.thy	Mon Mar 23 08:14:24 2009 +0100
    24.3 @@ -1,11 +1,9 @@
    24.4 -(*  ID:         $Id$
    24.5 -    Author:     Tobias Nipkow, 2007
    24.6 -*)
    24.7 +(*  Author: Tobias Nipkow, 2007 *)
    24.8  
    24.9 -header "Lists as vectors"
   24.10 +header {* Lists as vectors *}
   24.11  
   24.12  theory ListVector
   24.13 -imports Plain "~~/src/HOL/List"
   24.14 +imports List Main
   24.15  begin
   24.16  
   24.17  text{* \noindent
    25.1 --- a/src/HOL/Library/List_Prefix.thy	Mon Mar 23 08:14:23 2009 +0100
    25.2 +++ b/src/HOL/Library/List_Prefix.thy	Mon Mar 23 08:14:24 2009 +0100
    25.3 @@ -1,12 +1,11 @@
    25.4  (*  Title:      HOL/Library/List_Prefix.thy
    25.5 -    ID:         $Id$
    25.6      Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
    25.7  *)
    25.8  
    25.9  header {* List prefixes and postfixes *}
   25.10  
   25.11  theory List_Prefix
   25.12 -imports Plain "~~/src/HOL/List"
   25.13 +imports List Main
   25.14  begin
   25.15  
   25.16  subsection {* Prefix order on lists *}
    26.1 --- a/src/HOL/Library/List_lexord.thy	Mon Mar 23 08:14:23 2009 +0100
    26.2 +++ b/src/HOL/Library/List_lexord.thy	Mon Mar 23 08:14:24 2009 +0100
    26.3 @@ -1,12 +1,11 @@
    26.4  (*  Title:      HOL/Library/List_lexord.thy
    26.5 -    ID:         $Id$
    26.6      Author:     Norbert Voelker
    26.7  *)
    26.8  
    26.9  header {* Lexicographic order on lists *}
   26.10  
   26.11  theory List_lexord
   26.12 -imports Plain "~~/src/HOL/List"
   26.13 +imports List Main
   26.14  begin
   26.15  
   26.16  instantiation list :: (ord) ord
    27.1 --- a/src/HOL/Library/Mapping.thy	Mon Mar 23 08:14:23 2009 +0100
    27.2 +++ b/src/HOL/Library/Mapping.thy	Mon Mar 23 08:14:24 2009 +0100
    27.3 @@ -5,7 +5,7 @@
    27.4  header {* An abstract view on maps for code generation. *}
    27.5  
    27.6  theory Mapping
    27.7 -imports Map
    27.8 +imports Map Main
    27.9  begin
   27.10  
   27.11  subsection {* Type definition and primitive operations *}
    28.1 --- a/src/HOL/Library/Multiset.thy	Mon Mar 23 08:14:23 2009 +0100
    28.2 +++ b/src/HOL/Library/Multiset.thy	Mon Mar 23 08:14:24 2009 +0100
    28.3 @@ -5,7 +5,7 @@
    28.4  header {* Multisets *}
    28.5  
    28.6  theory Multiset
    28.7 -imports Plain "~~/src/HOL/List"
    28.8 +imports List Main
    28.9  begin
   28.10  
   28.11  subsection {* The type of multisets *}
    29.1 --- a/src/HOL/Library/Nat_Infinity.thy	Mon Mar 23 08:14:23 2009 +0100
    29.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Mon Mar 23 08:14:24 2009 +0100
    29.3 @@ -5,7 +5,7 @@
    29.4  header {* Natural numbers with infinity *}
    29.5  
    29.6  theory Nat_Infinity
    29.7 -imports Plain "~~/src/HOL/Presburger"
    29.8 +imports Main
    29.9  begin
   29.10  
   29.11  subsection {* Type definition *}
    30.1 --- a/src/HOL/Library/Nat_Int_Bij.thy	Mon Mar 23 08:14:23 2009 +0100
    30.2 +++ b/src/HOL/Library/Nat_Int_Bij.thy	Mon Mar 23 08:14:24 2009 +0100
    30.3 @@ -1,12 +1,11 @@
    30.4  (*  Title:      HOL/Nat_Int_Bij.thy
    30.5 -    ID:         $Id$
    30.6      Author:     Stefan Richter, Tobias Nipkow
    30.7  *)
    30.8  
    30.9  header{* Bijections $\mathbb{N}\to\mathbb{N}^2$ and $\mathbb{N}\to\mathbb{Z}$*}
   30.10  
   30.11  theory Nat_Int_Bij
   30.12 -imports Hilbert_Choice Presburger
   30.13 +imports Main
   30.14  begin
   30.15  
   30.16  subsection{*  A bijection between @{text "\<nat>"} and @{text "\<nat>\<twosuperior>"} *}
    31.1 --- a/src/HOL/Library/Nested_Environment.thy	Mon Mar 23 08:14:23 2009 +0100
    31.2 +++ b/src/HOL/Library/Nested_Environment.thy	Mon Mar 23 08:14:24 2009 +0100
    31.3 @@ -1,12 +1,11 @@
    31.4  (*  Title:      HOL/Library/Nested_Environment.thy
    31.5 -    ID:         $Id$
    31.6      Author:     Markus Wenzel, TU Muenchen
    31.7  *)
    31.8  
    31.9  header {* Nested environments *}
   31.10  
   31.11  theory Nested_Environment
   31.12 -imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Eval"
   31.13 +imports Main
   31.14  begin
   31.15  
   31.16  text {*
    32.1 --- a/src/HOL/Library/Numeral_Type.thy	Mon Mar 23 08:14:23 2009 +0100
    32.2 +++ b/src/HOL/Library/Numeral_Type.thy	Mon Mar 23 08:14:24 2009 +0100
    32.3 @@ -5,7 +5,7 @@
    32.4  header {* Numeral Syntax for Types *}
    32.5  
    32.6  theory Numeral_Type
    32.7 -imports Plain "~~/src/HOL/Presburger"
    32.8 +imports Main
    32.9  begin
   32.10  
   32.11  subsection {* Preliminary lemmas *}
    33.1 --- a/src/HOL/Library/OptionalSugar.thy	Mon Mar 23 08:14:23 2009 +0100
    33.2 +++ b/src/HOL/Library/OptionalSugar.thy	Mon Mar 23 08:14:24 2009 +0100
    33.3 @@ -4,7 +4,7 @@
    33.4  *)
    33.5  (*<*)
    33.6  theory OptionalSugar
    33.7 -imports LaTeXsugar Complex_Main
    33.8 +imports Complex_Main LaTeXsugar
    33.9  begin
   33.10  
   33.11  (* hiding set *)
    34.1 --- a/src/HOL/Library/Permutations.thy	Mon Mar 23 08:14:23 2009 +0100
    34.2 +++ b/src/HOL/Library/Permutations.thy	Mon Mar 23 08:14:24 2009 +0100
    34.3 @@ -5,7 +5,7 @@
    34.4  header {* Permutations, both general and specifically on finite sets.*}
    34.5  
    34.6  theory Permutations
    34.7 -imports Main Finite_Cartesian_Product Parity Fact
    34.8 +imports Finite_Cartesian_Product Parity Fact Main
    34.9  begin
   34.10  
   34.11    (* Why should I import Main just to solve the Typerep problem! *)
    35.1 --- a/src/HOL/Library/Zorn.thy	Mon Mar 23 08:14:23 2009 +0100
    35.2 +++ b/src/HOL/Library/Zorn.thy	Mon Mar 23 08:14:24 2009 +0100
    35.3 @@ -7,7 +7,7 @@
    35.4  header {* Zorn's Lemma *}
    35.5  
    35.6  theory Zorn
    35.7 -imports "~~/src/HOL/Order_Relation"
    35.8 +imports Order_Relation Main
    35.9  begin
   35.10  
   35.11  (* Define globally? In Set.thy? *)