--- a/src/HOL/NSA/HSEQ.thy Tue Mar 26 12:20:57 2013 +0100
+++ b/src/HOL/NSA/HSEQ.thy Tue Mar 26 12:20:58 2013 +0100
@@ -9,7 +9,7 @@
header {* Sequences and Convergence (Nonstandard) *}
theory HSEQ
-imports SEQ NatStar
+imports Limits NatStar
begin
definition