--- a/src/HOL/Hyperreal/Deriv.thy Thu Apr 12 02:59:44 2007 +0200
+++ b/src/HOL/Hyperreal/Deriv.thy Thu Apr 12 03:37:30 2007 +0200
@@ -9,7 +9,7 @@
header{* Differentiation *}
theory Deriv
-imports Lim
+imports HLim
begin
text{*Standard and Nonstandard Definitions*}