# HG changeset patch
# User blanchet
# Date 1385643492 -3600
# Node ID a8ad7f6dd217f8595f8a4d5c7f72e7a7a3c3b801
# Parent  0cb8a2defb06f6b835d5418dcc26d3002e748f9b
reduce dependency (toward move to 'HOL')

diff -r 0cb8a2defb06 -r a8ad7f6dd217 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Thu Nov 28 13:58:11 2013 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Thu Nov 28 13:58:12 2013 +0100
@@ -5,7 +5,7 @@
 header {* Infinite Sets and Related Concepts *}
 
 theory Infinite_Set
-imports Main
+imports Set_Interval
 begin
 
 subsection "Infinite Sets"
@@ -554,4 +554,3 @@
   by (simp add: atmost_one_def)
 
 end
-