--- a/src/HOL/Library/Binomial.thy Tue Dec 18 12:26:24 2007 +0100
+++ b/src/HOL/Library/Binomial.thy Tue Dec 18 14:37:00 2007 +0100
@@ -7,7 +7,7 @@
header {* Binomial Coefficients *}
theory Binomial
-imports PreList
+imports ATP_Linkup
begin
text {* This development is based on the work of Andy Gordon and
--- a/src/HOL/Library/Boolean_Algebra.thy Tue Dec 18 12:26:24 2007 +0100
+++ b/src/HOL/Library/Boolean_Algebra.thy Tue Dec 18 14:37:00 2007 +0100
@@ -8,7 +8,7 @@
header {* Boolean Algebras *}
theory Boolean_Algebra
-imports PreList
+imports ATP_Linkup
begin
locale boolean =
--- a/src/HOL/Library/Code_Index.thy Tue Dec 18 12:26:24 2007 +0100
+++ b/src/HOL/Library/Code_Index.thy Tue Dec 18 14:37:00 2007 +0100
@@ -5,7 +5,7 @@
header {* Type of indices *}
theory Code_Index
-imports PreList
+imports ATP_Linkup
begin
text {*
--- a/src/HOL/Library/Continuity.thy Tue Dec 18 12:26:24 2007 +0100
+++ b/src/HOL/Library/Continuity.thy Tue Dec 18 14:37:00 2007 +0100
@@ -6,7 +6,7 @@
header {* Continuity and iterations (of set transformers) *}
theory Continuity
-imports PreList
+imports ATP_Linkup
begin
subsection {* Continuity for complete lattices *}
--- a/src/HOL/Library/Eval.thy Tue Dec 18 12:26:24 2007 +0100
+++ b/src/HOL/Library/Eval.thy Tue Dec 18 14:37:00 2007 +0100
@@ -6,7 +6,7 @@
header {* A simple term evaluation mechanism *}
theory Eval
-imports PreList Pure_term
+imports ATP_Linkup Pure_term
begin
subsection {* @{text typ_of} class *}
--- a/src/HOL/Library/NatPair.thy Tue Dec 18 12:26:24 2007 +0100
+++ b/src/HOL/Library/NatPair.thy Tue Dec 18 14:37:00 2007 +0100
@@ -7,7 +7,7 @@
header {* Pairs of Natural Numbers *}
theory NatPair
-imports PreList
+imports ATP_Linkup
begin
text{*
--- a/src/HOL/Library/Nat_Infinity.thy Tue Dec 18 12:26:24 2007 +0100
+++ b/src/HOL/Library/Nat_Infinity.thy Tue Dec 18 14:37:00 2007 +0100
@@ -6,7 +6,7 @@
header {* Natural numbers with infinity *}
theory Nat_Infinity
-imports PreList
+imports ATP_Linkup
begin
subsection "Definitions"
--- a/src/HOL/Library/Parity.thy Tue Dec 18 12:26:24 2007 +0100
+++ b/src/HOL/Library/Parity.thy Tue Dec 18 14:37:00 2007 +0100
@@ -6,7 +6,7 @@
header {* Even and Odd for int and nat *}
theory Parity
-imports PreList
+imports ATP_Linkup
begin
class even_odd = type +
--- a/src/HOL/Library/Product_ord.thy Tue Dec 18 12:26:24 2007 +0100
+++ b/src/HOL/Library/Product_ord.thy Tue Dec 18 14:37:00 2007 +0100
@@ -6,7 +6,7 @@
header {* Order on product types *}
theory Product_ord
-imports PreList
+imports ATP_Linkup
begin
instantiation "*" :: (ord, ord) ord
--- a/src/HOL/Library/Quotient.thy Tue Dec 18 12:26:24 2007 +0100
+++ b/src/HOL/Library/Quotient.thy Tue Dec 18 14:37:00 2007 +0100
@@ -6,7 +6,7 @@
header {* Quotient types *}
theory Quotient
-imports PreList Hilbert_Choice
+imports ATP_Linkup Hilbert_Choice
begin
text {*
--- a/src/HOL/Library/Ramsey.thy Tue Dec 18 12:26:24 2007 +0100
+++ b/src/HOL/Library/Ramsey.thy Tue Dec 18 14:37:00 2007 +0100
@@ -6,7 +6,7 @@
header "Ramsey's Theorem"
theory Ramsey
-imports PreList Infinite_Set
+imports ATP_Linkup Infinite_Set
begin
subsection {* Preliminaries *}
--- a/src/HOL/Library/SetsAndFunctions.thy Tue Dec 18 12:26:24 2007 +0100
+++ b/src/HOL/Library/SetsAndFunctions.thy Tue Dec 18 14:37:00 2007 +0100
@@ -6,7 +6,7 @@
header {* Operations on sets and functions *}
theory SetsAndFunctions
-imports PreList
+imports ATP_Linkup
begin
text {*
--- a/src/HOL/Library/Zorn.thy Tue Dec 18 12:26:24 2007 +0100
+++ b/src/HOL/Library/Zorn.thy Tue Dec 18 14:37:00 2007 +0100
@@ -7,7 +7,7 @@
header {* Zorn's Lemma *}
theory Zorn
-imports PreList Hilbert_Choice
+imports ATP_Linkup Hilbert_Choice
begin
text{*