
diff -r ef8c7c5eb01b -r ea2707645af8 src/HOL/Infinite_Set.thy
--- a/src/HOL/Infinite_Set.thy	Thu Mar 25 10:31:25 2004 +0100
+++ b/src/HOL/Infinite_Set.thy	Thu Mar 25 10:32:21 2004 +0100
@@ -5,7 +5,7 @@
 
 header {* Infnite Sets and Related Concepts*}
 
-theory Infinite_Set = Hilbert_Choice + Finite_Set:
+theory Infinite_Set = Hilbert_Choice + Finite_Set + SetInterval:
 
 subsection "Infinite Sets"
 




