# HG changeset patch
# User paulson
# Date 1197911481 -3600
# Node ID 5e9d6f77d11afd911833d810a27382410c193b0c
# Parent  497474b69c8674861fe9bc7a9ca281bbfef6270e
fixed ancestors

diff -r 497474b69c86 -r 5e9d6f77d11a src/HOL/Library/GCD.thy
--- a/src/HOL/Library/GCD.thy	Mon Dec 17 18:01:51 2007 +0100
+++ b/src/HOL/Library/GCD.thy	Mon Dec 17 18:11:21 2007 +0100
@@ -7,7 +7,7 @@
 header {* The Greatest Common Divisor *}
 
 theory GCD
-imports PreList
+imports ATP_Linkup
 begin
 
 text {*
diff -r 497474b69c86 -r 5e9d6f77d11a src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Mon Dec 17 18:01:51 2007 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Mon Dec 17 18:11:21 2007 +0100
@@ -6,7 +6,7 @@
 header {* Infinite Sets and Related Concepts *}
 
 theory Infinite_Set
-imports PreList Hilbert_Choice
+imports ATP_Linkup
 begin
 
 subsection "Infinite Sets"