switched import from Main to PreList
authorhaftmann
Mon Dec 10 11:24:09 2007 +0100 (2007-12-10)
changeset 2559443c718438f9f
parent 25593 0b0df6c8646a
child 25595 6c48275f9c76
switched import from Main to PreList
src/HOL/Library/Binomial.thy
src/HOL/Library/Boolean_Algebra.thy
src/HOL/Library/Continuity.thy
src/HOL/Library/Eval.thy
src/HOL/Library/GCD.thy
src/HOL/Library/Infinite_Set.thy
src/HOL/Library/NatPair.thy
src/HOL/Library/Nat_Infinity.thy
src/HOL/Library/Parity.thy
src/HOL/Library/Product_ord.thy
src/HOL/Library/Quotient.thy
src/HOL/Library/Ramsey.thy
src/HOL/Library/SetsAndFunctions.thy
src/HOL/Library/Zorn.thy
     1.1 --- a/src/HOL/Library/Binomial.thy	Mon Dec 10 11:24:08 2007 +0100
     1.2 +++ b/src/HOL/Library/Binomial.thy	Mon Dec 10 11:24:09 2007 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  header {* Binomial Coefficients *}
     1.5  
     1.6  theory Binomial
     1.7 -imports Main
     1.8 +imports PreList
     1.9  begin
    1.10  
    1.11  text {* This development is based on the work of Andy Gordon and
     2.1 --- a/src/HOL/Library/Boolean_Algebra.thy	Mon Dec 10 11:24:08 2007 +0100
     2.2 +++ b/src/HOL/Library/Boolean_Algebra.thy	Mon Dec 10 11:24:09 2007 +0100
     2.3 @@ -8,7 +8,7 @@
     2.4  header {* Boolean Algebras *}
     2.5  
     2.6  theory Boolean_Algebra
     2.7 -imports Main
     2.8 +imports PreList
     2.9  begin
    2.10  
    2.11  locale boolean =
     3.1 --- a/src/HOL/Library/Continuity.thy	Mon Dec 10 11:24:08 2007 +0100
     3.2 +++ b/src/HOL/Library/Continuity.thy	Mon Dec 10 11:24:09 2007 +0100
     3.3 @@ -6,7 +6,7 @@
     3.4  header {* Continuity and iterations (of set transformers) *}
     3.5  
     3.6  theory Continuity
     3.7 -imports Main
     3.8 +imports PreList
     3.9  begin
    3.10  
    3.11  subsection {* Continuity for complete lattices *}
     4.1 --- a/src/HOL/Library/Eval.thy	Mon Dec 10 11:24:08 2007 +0100
     4.2 +++ b/src/HOL/Library/Eval.thy	Mon Dec 10 11:24:09 2007 +0100
     4.3 @@ -6,7 +6,7 @@
     4.4  header {* A simple term evaluation mechanism *}
     4.5  
     4.6  theory Eval
     4.7 -imports Main Pure_term
     4.8 +imports PreList Pure_term
     4.9  begin
    4.10  
    4.11  subsection {* @{text typ_of} class *}
     5.1 --- a/src/HOL/Library/GCD.thy	Mon Dec 10 11:24:08 2007 +0100
     5.2 +++ b/src/HOL/Library/GCD.thy	Mon Dec 10 11:24:09 2007 +0100
     5.3 @@ -7,7 +7,7 @@
     5.4  header {* The Greatest Common Divisor *}
     5.5  
     5.6  theory GCD
     5.7 -imports Main
     5.8 +imports PreList
     5.9  begin
    5.10  
    5.11  text {*
     6.1 --- a/src/HOL/Library/Infinite_Set.thy	Mon Dec 10 11:24:08 2007 +0100
     6.2 +++ b/src/HOL/Library/Infinite_Set.thy	Mon Dec 10 11:24:09 2007 +0100
     6.3 @@ -6,7 +6,7 @@
     6.4  header {* Infinite Sets and Related Concepts *}
     6.5  
     6.6  theory Infinite_Set
     6.7 -imports Main
     6.8 +imports PreList Hilbert_Choice
     6.9  begin
    6.10  
    6.11  subsection "Infinite Sets"
     7.1 --- a/src/HOL/Library/NatPair.thy	Mon Dec 10 11:24:08 2007 +0100
     7.2 +++ b/src/HOL/Library/NatPair.thy	Mon Dec 10 11:24:09 2007 +0100
     7.3 @@ -7,7 +7,7 @@
     7.4  header {* Pairs of Natural Numbers *}
     7.5  
     7.6  theory NatPair
     7.7 -imports Main
     7.8 +imports PreList
     7.9  begin
    7.10  
    7.11  text{*
     8.1 --- a/src/HOL/Library/Nat_Infinity.thy	Mon Dec 10 11:24:08 2007 +0100
     8.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Mon Dec 10 11:24:09 2007 +0100
     8.3 @@ -6,7 +6,7 @@
     8.4  header {* Natural numbers with infinity *}
     8.5  
     8.6  theory Nat_Infinity
     8.7 -imports Main
     8.8 +imports PreList
     8.9  begin
    8.10  
    8.11  subsection "Definitions"
    8.12 @@ -25,19 +25,28 @@
    8.13  notation (HTML output)
    8.14    Infty  ("\<infinity>")
    8.15  
    8.16 -instance inat :: "{ord, zero}" ..
    8.17 -
    8.18  definition
    8.19    iSuc :: "inat => inat" where
    8.20    "iSuc i = (case i of Fin n => Fin (Suc n) | \<infinity> => \<infinity>)"
    8.21  
    8.22 -defs (overloaded)
    8.23 +instantiation inat :: "{ord, zero}"
    8.24 +begin
    8.25 +
    8.26 +definition
    8.27    Zero_inat_def: "0 == Fin 0"
    8.28 +
    8.29 +definition
    8.30    iless_def: "m < n ==
    8.31      case m of Fin m1 => (case n of Fin n1 => m1 < n1 | \<infinity> => True)
    8.32      | \<infinity>  => False"
    8.33 +
    8.34 +definition
    8.35    ile_def: "(m::inat) \<le> n == \<not> (n < m)"
    8.36  
    8.37 +instance ..
    8.38 +
    8.39 +end
    8.40 +
    8.41  lemmas inat_defs = Zero_inat_def iSuc_def iless_def ile_def
    8.42  lemmas inat_splits = inat.split inat.split_asm
    8.43  
     9.1 --- a/src/HOL/Library/Parity.thy	Mon Dec 10 11:24:08 2007 +0100
     9.2 +++ b/src/HOL/Library/Parity.thy	Mon Dec 10 11:24:09 2007 +0100
     9.3 @@ -6,7 +6,7 @@
     9.4  header {* Even and Odd for int and nat *}
     9.5  
     9.6  theory Parity
     9.7 -imports Main
     9.8 +imports PreList
     9.9  begin
    9.10  
    9.11  class even_odd = type + 
    10.1 --- a/src/HOL/Library/Product_ord.thy	Mon Dec 10 11:24:08 2007 +0100
    10.2 +++ b/src/HOL/Library/Product_ord.thy	Mon Dec 10 11:24:09 2007 +0100
    10.3 @@ -6,7 +6,7 @@
    10.4  header {* Order on product types *}
    10.5  
    10.6  theory Product_ord
    10.7 -imports Main
    10.8 +imports PreList
    10.9  begin
   10.10  
   10.11  instantiation "*" :: (ord, ord) ord
    11.1 --- a/src/HOL/Library/Quotient.thy	Mon Dec 10 11:24:08 2007 +0100
    11.2 +++ b/src/HOL/Library/Quotient.thy	Mon Dec 10 11:24:09 2007 +0100
    11.3 @@ -6,7 +6,7 @@
    11.4  header {* Quotient types *}
    11.5  
    11.6  theory Quotient
    11.7 -imports Main
    11.8 +imports PreList Hilbert_Choice
    11.9  begin
   11.10  
   11.11  text {*
    12.1 --- a/src/HOL/Library/Ramsey.thy	Mon Dec 10 11:24:08 2007 +0100
    12.2 +++ b/src/HOL/Library/Ramsey.thy	Mon Dec 10 11:24:09 2007 +0100
    12.3 @@ -5,7 +5,9 @@
    12.4  
    12.5  header "Ramsey's Theorem"
    12.6  
    12.7 -theory Ramsey imports Main Infinite_Set begin
    12.8 +theory Ramsey
    12.9 +imports PreList Infinite_Set
   12.10 +begin
   12.11  
   12.12  subsection {* Preliminaries *}
   12.13  
    13.1 --- a/src/HOL/Library/SetsAndFunctions.thy	Mon Dec 10 11:24:08 2007 +0100
    13.2 +++ b/src/HOL/Library/SetsAndFunctions.thy	Mon Dec 10 11:24:09 2007 +0100
    13.3 @@ -6,7 +6,7 @@
    13.4  header {* Operations on sets and functions *}
    13.5  
    13.6  theory SetsAndFunctions
    13.7 -imports Main
    13.8 +imports PreList
    13.9  begin
   13.10  
   13.11  text {*
   13.12 @@ -17,39 +17,98 @@
   13.13  
   13.14  subsection {* Basic definitions *}
   13.15  
   13.16 -instance set :: (plus) plus ..
   13.17 -instance "fun" :: (type, plus) plus ..
   13.18 +instantiation set :: (plus) plus
   13.19 +begin
   13.20  
   13.21 -defs (overloaded)
   13.22 -  func_plus: "f + g == (%x. f x + g x)"
   13.23 +definition
   13.24    set_plus: "A + B == {c. EX a:A. EX b:B. c = a + b}"
   13.25  
   13.26 -instance set :: (times) times ..
   13.27 -instance "fun" :: (type, times) times ..
   13.28 +instance ..
   13.29 +
   13.30 +end
   13.31 +
   13.32 +instantiation "fun" :: (type, plus) plus
   13.33 +begin
   13.34  
   13.35 -defs (overloaded)
   13.36 -  func_times: "f * g == (%x. f x * g x)"
   13.37 +definition
   13.38 +  func_plus: "f + g == (%x. f x + g x)"
   13.39 +
   13.40 +instance ..
   13.41 +
   13.42 +end
   13.43 +
   13.44 +instantiation set :: (times) times
   13.45 +begin
   13.46 +
   13.47 +definition
   13.48    set_times:"A * B == {c. EX a:A. EX b:B. c = a * b}"
   13.49  
   13.50 -instance "fun" :: (type, minus) minus ..
   13.51 +instance ..
   13.52 +
   13.53 +end
   13.54 +
   13.55 +instantiation "fun" :: (type, times) times
   13.56 +begin
   13.57 +
   13.58 +definition
   13.59 +  func_times: "f * g == (%x. f x * g x)"
   13.60  
   13.61 -defs (overloaded)
   13.62 +instance ..
   13.63 +
   13.64 +end
   13.65 +
   13.66 +instantiation "fun" :: (type, minus) minus
   13.67 +begin
   13.68 +
   13.69 +definition
   13.70    func_minus: "- f == (%x. - f x)"
   13.71 +
   13.72 +definition
   13.73    func_diff: "f - g == %x. f x - g x"
   13.74  
   13.75 -instance "fun" :: (type, zero) zero ..
   13.76 -instance set :: (zero) zero ..
   13.77 +instance ..
   13.78 +
   13.79 +end
   13.80  
   13.81 -defs (overloaded)
   13.82 -  func_zero: "0::(('a::type) => ('b::zero)) == %x. 0"
   13.83 +instantiation set :: (zero) zero
   13.84 +begin
   13.85 +
   13.86 +definition
   13.87    set_zero: "0::('a::zero)set == {0}"
   13.88  
   13.89 -instance "fun" :: (type, one) one ..
   13.90 -instance set :: (one) one ..
   13.91 +instance ..
   13.92 +
   13.93 +end
   13.94 +
   13.95 +instantiation "fun" :: (type, zero) zero
   13.96 +begin
   13.97 +
   13.98 +definition
   13.99 +  func_zero: "0::(('a::type) => ('b::zero)) == %x. 0"
  13.100 +
  13.101 +instance ..
  13.102 +
  13.103 +end
  13.104 +
  13.105 +instantiation set :: (one) one
  13.106 +begin
  13.107  
  13.108 -defs (overloaded)
  13.109 +definition
  13.110 +  set_one: "1::('a::one)set == {1}"
  13.111 +
  13.112 +instance ..
  13.113 +
  13.114 +end
  13.115 +
  13.116 +instantiation "fun" :: (type, one) one
  13.117 +begin
  13.118 +
  13.119 +definition
  13.120    func_one: "1::(('a::type) => ('b::one)) == %x. 1"
  13.121 -  set_one: "1::('a::one)set == {1}"
  13.122 +
  13.123 +instance ..
  13.124 +
  13.125 +end
  13.126  
  13.127  definition
  13.128    elt_set_plus :: "'a::plus => 'a set => 'a set"  (infixl "+o" 70) where
    14.1 --- a/src/HOL/Library/Zorn.thy	Mon Dec 10 11:24:08 2007 +0100
    14.2 +++ b/src/HOL/Library/Zorn.thy	Mon Dec 10 11:24:09 2007 +0100
    14.3 @@ -7,7 +7,7 @@
    14.4  header {* Zorn's Lemma *}
    14.5  
    14.6  theory Zorn
    14.7 -imports Main
    14.8 +imports PreList Hilbert_Choice
    14.9  begin
   14.10  
   14.11  text{*