src/HOL/Nonstandard_Analysis/HSEQ.thy

--- a/src/HOL/Nonstandard_Analysis/HSEQ.thy	Fri Aug 18 13:55:05 2017 +0200
+++ b/src/HOL/Nonstandard_Analysis/HSEQ.thy	Fri Aug 18 20:47:47 2017 +0200
@@ -11,7 +11,7 @@
 section \<open>Sequences and Convergence (Nonstandard)\<close>
 
 theory HSEQ
-  imports Limits NatStar
+  imports HOL.Limits NatStar
   abbrevs "--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S"
 begin