--- a/src/HOL/Lim.thy Mon Dec 29 13:23:53 2008 +0100
+++ b/src/HOL/Lim.thy Mon Dec 29 14:08:08 2008 +0100
@@ -7,7 +7,7 @@
header{* Limits and Continuity *}
theory Lim
-imports "~~/src/HOL/Hyperreal/SEQ"
+imports SEQ
begin
text{*Standard Definitions*}