# HG changeset patch
# User haftmann
# Date 1197282249 -3600
# Node ID 43c718438f9f46a69adb708e2a413a2f90dc5a90
# Parent  0b0df6c8646aaf8219003e2ed7f4a284e1909721
switched import from Main to PreList

diff -r 0b0df6c8646a -r 43c718438f9f src/HOL/Library/Binomial.thy
--- a/src/HOL/Library/Binomial.thy	Mon Dec 10 11:24:08 2007 +0100
+++ b/src/HOL/Library/Binomial.thy	Mon Dec 10 11:24:09 2007 +0100
@@ -7,7 +7,7 @@
 header {* Binomial Coefficients *}
 
 theory Binomial
-imports Main
+imports PreList
 begin
 
 text {* This development is based on the work of Andy Gordon and
diff -r 0b0df6c8646a -r 43c718438f9f src/HOL/Library/Boolean_Algebra.thy
--- a/src/HOL/Library/Boolean_Algebra.thy	Mon Dec 10 11:24:08 2007 +0100
+++ b/src/HOL/Library/Boolean_Algebra.thy	Mon Dec 10 11:24:09 2007 +0100
@@ -8,7 +8,7 @@
 header {* Boolean Algebras *}
 
 theory Boolean_Algebra
-imports Main
+imports PreList
 begin
 
 locale boolean =
diff -r 0b0df6c8646a -r 43c718438f9f src/HOL/Library/Continuity.thy
--- a/src/HOL/Library/Continuity.thy	Mon Dec 10 11:24:08 2007 +0100
+++ b/src/HOL/Library/Continuity.thy	Mon Dec 10 11:24:09 2007 +0100
@@ -6,7 +6,7 @@
 header {* Continuity and iterations (of set transformers) *}
 
 theory Continuity
-imports Main
+imports PreList
 begin
 
 subsection {* Continuity for complete lattices *}
diff -r 0b0df6c8646a -r 43c718438f9f src/HOL/Library/Eval.thy
--- a/src/HOL/Library/Eval.thy	Mon Dec 10 11:24:08 2007 +0100
+++ b/src/HOL/Library/Eval.thy	Mon Dec 10 11:24:09 2007 +0100
@@ -6,7 +6,7 @@
 header {* A simple term evaluation mechanism *}
 
 theory Eval
-imports Main Pure_term
+imports PreList Pure_term
 begin
 
 subsection {* @{text typ_of} class *}
diff -r 0b0df6c8646a -r 43c718438f9f src/HOL/Library/GCD.thy
--- a/src/HOL/Library/GCD.thy	Mon Dec 10 11:24:08 2007 +0100
+++ b/src/HOL/Library/GCD.thy	Mon Dec 10 11:24:09 2007 +0100
@@ -7,7 +7,7 @@
 header {* The Greatest Common Divisor *}
 
 theory GCD
-imports Main
+imports PreList
 begin
 
 text {*
diff -r 0b0df6c8646a -r 43c718438f9f src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Mon Dec 10 11:24:08 2007 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Mon Dec 10 11:24:09 2007 +0100
@@ -6,7 +6,7 @@
 header {* Infinite Sets and Related Concepts *}
 
 theory Infinite_Set
-imports Main
+imports PreList Hilbert_Choice
 begin
 
 subsection "Infinite Sets"
diff -r 0b0df6c8646a -r 43c718438f9f src/HOL/Library/NatPair.thy
--- a/src/HOL/Library/NatPair.thy	Mon Dec 10 11:24:08 2007 +0100
+++ b/src/HOL/Library/NatPair.thy	Mon Dec 10 11:24:09 2007 +0100
@@ -7,7 +7,7 @@
 header {* Pairs of Natural Numbers *}
 
 theory NatPair
-imports Main
+imports PreList
 begin
 
 text{*
diff -r 0b0df6c8646a -r 43c718438f9f src/HOL/Library/Nat_Infinity.thy
--- a/src/HOL/Library/Nat_Infinity.thy	Mon Dec 10 11:24:08 2007 +0100
+++ b/src/HOL/Library/Nat_Infinity.thy	Mon Dec 10 11:24:09 2007 +0100
@@ -6,7 +6,7 @@
 header {* Natural numbers with infinity *}
 
 theory Nat_Infinity
-imports Main
+imports PreList
 begin
 
 subsection "Definitions"
@@ -25,19 +25,28 @@
 notation (HTML output)
   Infty  ("\<infinity>")
 
-instance inat :: "{ord, zero}" ..
-
 definition
   iSuc :: "inat => inat" where
   "iSuc i = (case i of Fin n => Fin (Suc n) | \<infinity> => \<infinity>)"
 
-defs (overloaded)
+instantiation inat :: "{ord, zero}"
+begin
+
+definition
   Zero_inat_def: "0 == Fin 0"
+
+definition
   iless_def: "m < n ==
     case m of Fin m1 => (case n of Fin n1 => m1 < n1 | \<infinity> => True)
     | \<infinity>  => False"
+
+definition
   ile_def: "(m::inat) \<le> n == \<not> (n < m)"
 
+instance ..
+
+end
+
 lemmas inat_defs = Zero_inat_def iSuc_def iless_def ile_def
 lemmas inat_splits = inat.split inat.split_asm
 
diff -r 0b0df6c8646a -r 43c718438f9f src/HOL/Library/Parity.thy
--- a/src/HOL/Library/Parity.thy	Mon Dec 10 11:24:08 2007 +0100
+++ b/src/HOL/Library/Parity.thy	Mon Dec 10 11:24:09 2007 +0100
@@ -6,7 +6,7 @@
 header {* Even and Odd for int and nat *}
 
 theory Parity
-imports Main
+imports PreList
 begin
 
 class even_odd = type + 
diff -r 0b0df6c8646a -r 43c718438f9f src/HOL/Library/Product_ord.thy
--- a/src/HOL/Library/Product_ord.thy	Mon Dec 10 11:24:08 2007 +0100
+++ b/src/HOL/Library/Product_ord.thy	Mon Dec 10 11:24:09 2007 +0100
@@ -6,7 +6,7 @@
 header {* Order on product types *}
 
 theory Product_ord
-imports Main
+imports PreList
 begin
 
 instantiation "*" :: (ord, ord) ord
diff -r 0b0df6c8646a -r 43c718438f9f src/HOL/Library/Quotient.thy
--- a/src/HOL/Library/Quotient.thy	Mon Dec 10 11:24:08 2007 +0100
+++ b/src/HOL/Library/Quotient.thy	Mon Dec 10 11:24:09 2007 +0100
@@ -6,7 +6,7 @@
 header {* Quotient types *}
 
 theory Quotient
-imports Main
+imports PreList Hilbert_Choice
 begin
 
 text {*
diff -r 0b0df6c8646a -r 43c718438f9f src/HOL/Library/Ramsey.thy
--- a/src/HOL/Library/Ramsey.thy	Mon Dec 10 11:24:08 2007 +0100
+++ b/src/HOL/Library/Ramsey.thy	Mon Dec 10 11:24:09 2007 +0100
@@ -5,7 +5,9 @@
 
 header "Ramsey's Theorem"
 
-theory Ramsey imports Main Infinite_Set begin
+theory Ramsey
+imports PreList Infinite_Set
+begin
 
 subsection {* Preliminaries *}
 
diff -r 0b0df6c8646a -r 43c718438f9f src/HOL/Library/SetsAndFunctions.thy
--- a/src/HOL/Library/SetsAndFunctions.thy	Mon Dec 10 11:24:08 2007 +0100
+++ b/src/HOL/Library/SetsAndFunctions.thy	Mon Dec 10 11:24:09 2007 +0100
@@ -6,7 +6,7 @@
 header {* Operations on sets and functions *}
 
 theory SetsAndFunctions
-imports Main
+imports PreList
 begin
 
 text {*
@@ -17,39 +17,98 @@
 
 subsection {* Basic definitions *}
 
-instance set :: (plus) plus ..
-instance "fun" :: (type, plus) plus ..
+instantiation set :: (plus) plus
+begin
 
-defs (overloaded)
-  func_plus: "f + g == (%x. f x + g x)"
+definition
   set_plus: "A + B == {c. EX a:A. EX b:B. c = a + b}"
 
-instance set :: (times) times ..
-instance "fun" :: (type, times) times ..
+instance ..
+
+end
+
+instantiation "fun" :: (type, plus) plus
+begin
 
-defs (overloaded)
-  func_times: "f * g == (%x. f x * g x)"
+definition
+  func_plus: "f + g == (%x. f x + g x)"
+
+instance ..
+
+end
+
+instantiation set :: (times) times
+begin
+
+definition
   set_times:"A * B == {c. EX a:A. EX b:B. c = a * b}"
 
-instance "fun" :: (type, minus) minus ..
+instance ..
+
+end
+
+instantiation "fun" :: (type, times) times
+begin
+
+definition
+  func_times: "f * g == (%x. f x * g x)"
 
-defs (overloaded)
+instance ..
+
+end
+
+instantiation "fun" :: (type, minus) minus
+begin
+
+definition
   func_minus: "- f == (%x. - f x)"
+
+definition
   func_diff: "f - g == %x. f x - g x"
 
-instance "fun" :: (type, zero) zero ..
-instance set :: (zero) zero ..
+instance ..
+
+end
 
-defs (overloaded)
-  func_zero: "0::(('a::type) => ('b::zero)) == %x. 0"
+instantiation set :: (zero) zero
+begin
+
+definition
   set_zero: "0::('a::zero)set == {0}"
 
-instance "fun" :: (type, one) one ..
-instance set :: (one) one ..
+instance ..
+
+end
+
+instantiation "fun" :: (type, zero) zero
+begin
+
+definition
+  func_zero: "0::(('a::type) => ('b::zero)) == %x. 0"
+
+instance ..
+
+end
+
+instantiation set :: (one) one
+begin
 
-defs (overloaded)
+definition
+  set_one: "1::('a::one)set == {1}"
+
+instance ..
+
+end
+
+instantiation "fun" :: (type, one) one
+begin
+
+definition
   func_one: "1::(('a::type) => ('b::one)) == %x. 1"
-  set_one: "1::('a::one)set == {1}"
+
+instance ..
+
+end
 
 definition
   elt_set_plus :: "'a::plus => 'a set => 'a set"  (infixl "+o" 70) where
diff -r 0b0df6c8646a -r 43c718438f9f src/HOL/Library/Zorn.thy
--- a/src/HOL/Library/Zorn.thy	Mon Dec 10 11:24:08 2007 +0100
+++ b/src/HOL/Library/Zorn.thy	Mon Dec 10 11:24:09 2007 +0100
@@ -7,7 +7,7 @@
 header {* Zorn's Lemma *}
 
 theory Zorn
-imports Main
+imports PreList Hilbert_Choice
 begin
 
 text{*