author | blanchet |
Thu, 28 Nov 2013 13:58:12 +0100 | |
changeset 54607 | a8ad7f6dd217 |
parent 54606 | 0cb8a2defb06 |
child 54608 | 48dadf69c44d |
--- 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 -