author | blanchet |
Thu, 28 Nov 2013 13:58:12 +0100 | |
changeset 55980 | a8ad7f6dd217 |
parent 55979 | 0cb8a2defb06 |
child 55981 | 48dadf69c44d |
1.1 --- a/src/HOL/Library/Infinite_Set.thy Thu Nov 28 13:58:11 2013 +0100 1.2 +++ b/src/HOL/Library/Infinite_Set.thy Thu Nov 28 13:58:12 2013 +0100 1.3 @@ -5,7 +5,7 @@ 1.4 header {* Infinite Sets and Related Concepts *} 1.5 1.6 theory Infinite_Set 1.7 -imports Main 1.8 +imports Set_Interval 1.9 begin 1.10 1.11 subsection "Infinite Sets" 1.12 @@ -554,4 +554,3 @@ 1.13 by (simp add: atmost_one_def) 1.14 1.15 end 1.16 -