--- 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