--- a/src/HOL/Hyperreal/SEQ.thy Fri Jul 11 09:02:24 2008 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy Fri Jul 11 09:02:26 2008 +0200
@@ -9,7 +9,7 @@
header {* Sequences and Convergence *}
theory SEQ
-imports "../Real/Real"
+imports "../Real/Real" "../Real/ContNotDenum"
begin
definition