src/HOL/Library/Infinite_Set.thy

--- a/src/HOL/Library/Infinite_Set.thy	Thu Jun 26 10:06:54 2008 +0200
+++ b/src/HOL/Library/Infinite_Set.thy	Thu Jun 26 10:07:01 2008 +0200
@@ -6,9 +6,10 @@
 header {* Infinite Sets and Related Concepts *}
 
 theory Infinite_Set
-imports ATP_Linkup
+imports Plain SetInterval Hilbert_Choice
 begin
 
+
 subsection "Infinite Sets"
 
 text {*