diff -r 31afce809794 -r 7e291ae244ea src/HOL/Library/Infinite_Set.thy --- 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 +