src/HOL/NSA/NSA.thy

--- a/src/HOL/NSA/NSA.thy	Tue Nov 05 09:45:00 2013 +0100
+++ b/src/HOL/NSA/NSA.thy	Tue Nov 05 09:45:02 2013 +0100
@@ -6,7 +6,7 @@
 header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*}
 
 theory NSA
-imports HyperDef
+imports HyperDef "~~/src/HOL/Library/Lubs_Glbs"
 begin
 
 definition