--- a/src/HOL/Hyperreal/HLim.thy Fri May 18 17:35:07 2007 +0200
+++ b/src/HOL/Hyperreal/HLim.thy Fri May 18 18:20:39 2007 +0200
@@ -8,7 +8,7 @@
header{* Limits and Continuity (Nonstandard) *}
theory HLim
-imports HSEQ Lim
+imports Star Lim
begin
text{*Nonstandard Definitions*}