--- a/src/HOL/RealVector.thy Tue May 11 17:20:11 2010 -0700
+++ b/src/HOL/RealVector.thy Tue May 11 18:06:58 2010 -0700
@@ -5,7 +5,7 @@
header {* Vector Spaces and Algebras over the Reals *}
theory RealVector
-imports RealPow
+imports RComplete
begin
subsection {* Locale for additive functions *}