--- 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
--- 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 =
--- 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 *}
--- 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 *}
--- 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 {*
--- 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"
--- 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{*
--- 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
--- 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 +
--- 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
--- 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 {*
--- 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 *}
--- 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
--- 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{*