src/HOL/Library/Infinite_Set.thy
changeset 54612 7e291ae244ea
parent 54607 a8ad7f6dd217
child 58881 b9556a055632
--- a/src/HOL/Library/Infinite_Set.thy	Fri Nov 29 08:26:45 2013 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Fri Nov 29 14:24:21 2013 +0100
@@ -5,7 +5,7 @@
 header {* Infinite Sets and Related Concepts *}
 
 theory Infinite_Set
-imports Set_Interval
+imports Main
 begin
 
 subsection "Infinite Sets"
@@ -554,3 +554,4 @@
   by (simp add: atmost_one_def)
 
 end
+