# HG changeset patch
# User haftmann
# Date 1197985020 -3600
# Node ID 8f8d83af100a82913d082d4ead00e83608c31be5
# Parent  5226396bf26159fd9f6d783d2677ba157d54114c
switched from PreList to ATP_Linkup

diff -r 5226396bf261 -r 8f8d83af100a src/HOL/Library/Binomial.thy
--- 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
diff -r 5226396bf261 -r 8f8d83af100a src/HOL/Library/Boolean_Algebra.thy
--- 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 =
diff -r 5226396bf261 -r 8f8d83af100a src/HOL/Library/Code_Index.thy
--- 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 {*
diff -r 5226396bf261 -r 8f8d83af100a src/HOL/Library/Continuity.thy
--- 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 *}
diff -r 5226396bf261 -r 8f8d83af100a src/HOL/Library/Eval.thy
--- 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 *}
diff -r 5226396bf261 -r 8f8d83af100a src/HOL/Library/NatPair.thy
--- 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{*
diff -r 5226396bf261 -r 8f8d83af100a src/HOL/Library/Nat_Infinity.thy
--- 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"
diff -r 5226396bf261 -r 8f8d83af100a src/HOL/Library/Parity.thy
--- 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 + 
diff -r 5226396bf261 -r 8f8d83af100a src/HOL/Library/Product_ord.thy
--- 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
diff -r 5226396bf261 -r 8f8d83af100a src/HOL/Library/Quotient.thy
--- 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 {*
diff -r 5226396bf261 -r 8f8d83af100a src/HOL/Library/Ramsey.thy
--- 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 *}
diff -r 5226396bf261 -r 8f8d83af100a src/HOL/Library/SetsAndFunctions.thy
--- 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 {*
diff -r 5226396bf261 -r 8f8d83af100a src/HOL/Library/Zorn.thy
--- 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{*