--- a/src/HOL/Real.thy Mon Dec 29 13:23:53 2008 +0100 +++ b/src/HOL/Real.thy Mon Dec 29 14:08:08 2008 +0100 @@ -1,5 +1,5 @@ theory Real -imports RComplete "~~/src/HOL/Real/RealVector" +imports RComplete RealVector begin end