switched from PreList to ATP_Linkup
authorhaftmann
Tue Dec 18 14:37:00 2007 +0100 (2007-12-18)
changeset 256918f8d83af100a
parent 25690 5226396bf261
child 25692 eda4958ab0d2
switched from PreList to ATP_Linkup
src/HOL/Library/Binomial.thy
src/HOL/Library/Boolean_Algebra.thy
src/HOL/Library/Code_Index.thy
src/HOL/Library/Continuity.thy
src/HOL/Library/Eval.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	Tue Dec 18 12:26:24 2007 +0100
     1.2 +++ b/src/HOL/Library/Binomial.thy	Tue Dec 18 14:37:00 2007 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  header {* Binomial Coefficients *}
     1.5  
     1.6  theory Binomial
     1.7 -imports PreList
     1.8 +imports ATP_Linkup
     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	Tue Dec 18 12:26:24 2007 +0100
     2.2 +++ b/src/HOL/Library/Boolean_Algebra.thy	Tue Dec 18 14:37:00 2007 +0100
     2.3 @@ -8,7 +8,7 @@
     2.4  header {* Boolean Algebras *}
     2.5  
     2.6  theory Boolean_Algebra
     2.7 -imports PreList
     2.8 +imports ATP_Linkup
     2.9  begin
    2.10  
    2.11  locale boolean =
     3.1 --- a/src/HOL/Library/Code_Index.thy	Tue Dec 18 12:26:24 2007 +0100
     3.2 +++ b/src/HOL/Library/Code_Index.thy	Tue Dec 18 14:37:00 2007 +0100
     3.3 @@ -5,7 +5,7 @@
     3.4  header {* Type of indices *}
     3.5  
     3.6  theory Code_Index
     3.7 -imports PreList
     3.8 +imports ATP_Linkup
     3.9  begin
    3.10  
    3.11  text {*
     4.1 --- a/src/HOL/Library/Continuity.thy	Tue Dec 18 12:26:24 2007 +0100
     4.2 +++ b/src/HOL/Library/Continuity.thy	Tue Dec 18 14:37:00 2007 +0100
     4.3 @@ -6,7 +6,7 @@
     4.4  header {* Continuity and iterations (of set transformers) *}
     4.5  
     4.6  theory Continuity
     4.7 -imports PreList
     4.8 +imports ATP_Linkup
     4.9  begin
    4.10  
    4.11  subsection {* Continuity for complete lattices *}
     5.1 --- a/src/HOL/Library/Eval.thy	Tue Dec 18 12:26:24 2007 +0100
     5.2 +++ b/src/HOL/Library/Eval.thy	Tue Dec 18 14:37:00 2007 +0100
     5.3 @@ -6,7 +6,7 @@
     5.4  header {* A simple term evaluation mechanism *}
     5.5  
     5.6  theory Eval
     5.7 -imports PreList Pure_term
     5.8 +imports ATP_Linkup Pure_term
     5.9  begin
    5.10  
    5.11  subsection {* @{text typ_of} class *}
     6.1 --- a/src/HOL/Library/NatPair.thy	Tue Dec 18 12:26:24 2007 +0100
     6.2 +++ b/src/HOL/Library/NatPair.thy	Tue Dec 18 14:37:00 2007 +0100
     6.3 @@ -7,7 +7,7 @@
     6.4  header {* Pairs of Natural Numbers *}
     6.5  
     6.6  theory NatPair
     6.7 -imports PreList
     6.8 +imports ATP_Linkup
     6.9  begin
    6.10  
    6.11  text{*
     7.1 --- a/src/HOL/Library/Nat_Infinity.thy	Tue Dec 18 12:26:24 2007 +0100
     7.2 +++ b/src/HOL/Library/Nat_Infinity.thy	Tue Dec 18 14:37:00 2007 +0100
     7.3 @@ -6,7 +6,7 @@
     7.4  header {* Natural numbers with infinity *}
     7.5  
     7.6  theory Nat_Infinity
     7.7 -imports PreList
     7.8 +imports ATP_Linkup
     7.9  begin
    7.10  
    7.11  subsection "Definitions"
     8.1 --- a/src/HOL/Library/Parity.thy	Tue Dec 18 12:26:24 2007 +0100
     8.2 +++ b/src/HOL/Library/Parity.thy	Tue Dec 18 14:37:00 2007 +0100
     8.3 @@ -6,7 +6,7 @@
     8.4  header {* Even and Odd for int and nat *}
     8.5  
     8.6  theory Parity
     8.7 -imports PreList
     8.8 +imports ATP_Linkup
     8.9  begin
    8.10  
    8.11  class even_odd = type + 
     9.1 --- a/src/HOL/Library/Product_ord.thy	Tue Dec 18 12:26:24 2007 +0100
     9.2 +++ b/src/HOL/Library/Product_ord.thy	Tue Dec 18 14:37:00 2007 +0100
     9.3 @@ -6,7 +6,7 @@
     9.4  header {* Order on product types *}
     9.5  
     9.6  theory Product_ord
     9.7 -imports PreList
     9.8 +imports ATP_Linkup
     9.9  begin
    9.10  
    9.11  instantiation "*" :: (ord, ord) ord
    10.1 --- a/src/HOL/Library/Quotient.thy	Tue Dec 18 12:26:24 2007 +0100
    10.2 +++ b/src/HOL/Library/Quotient.thy	Tue Dec 18 14:37:00 2007 +0100
    10.3 @@ -6,7 +6,7 @@
    10.4  header {* Quotient types *}
    10.5  
    10.6  theory Quotient
    10.7 -imports PreList Hilbert_Choice
    10.8 +imports ATP_Linkup Hilbert_Choice
    10.9  begin
   10.10  
   10.11  text {*
    11.1 --- a/src/HOL/Library/Ramsey.thy	Tue Dec 18 12:26:24 2007 +0100
    11.2 +++ b/src/HOL/Library/Ramsey.thy	Tue Dec 18 14:37:00 2007 +0100
    11.3 @@ -6,7 +6,7 @@
    11.4  header "Ramsey's Theorem"
    11.5  
    11.6  theory Ramsey
    11.7 -imports PreList Infinite_Set
    11.8 +imports ATP_Linkup Infinite_Set
    11.9  begin
   11.10  
   11.11  subsection {* Preliminaries *}
    12.1 --- a/src/HOL/Library/SetsAndFunctions.thy	Tue Dec 18 12:26:24 2007 +0100
    12.2 +++ b/src/HOL/Library/SetsAndFunctions.thy	Tue Dec 18 14:37:00 2007 +0100
    12.3 @@ -6,7 +6,7 @@
    12.4  header {* Operations on sets and functions *}
    12.5  
    12.6  theory SetsAndFunctions
    12.7 -imports PreList
    12.8 +imports ATP_Linkup
    12.9  begin
   12.10  
   12.11  text {*
    13.1 --- a/src/HOL/Library/Zorn.thy	Tue Dec 18 12:26:24 2007 +0100
    13.2 +++ b/src/HOL/Library/Zorn.thy	Tue Dec 18 14:37:00 2007 +0100
    13.3 @@ -7,7 +7,7 @@
    13.4  header {* Zorn's Lemma *}
    13.5  
    13.6  theory Zorn
    13.7 -imports PreList Hilbert_Choice
    13.8 +imports ATP_Linkup Hilbert_Choice
    13.9  begin
   13.10  
   13.11  text{*