--- a/src/HOL/Hyperreal/Filter.thy Sun Oct 01 18:29:25 2006 +0200
+++ b/src/HOL/Hyperreal/Filter.thy Sun Oct 01 18:29:26 2006 +0200
@@ -9,7 +9,7 @@
header {* Filters and Ultrafilters *}
theory Filter
-imports Zorn
+imports Zorn Infinite_Set
begin
subsection {* Definitions and basic properties *}