
diff -r 254478a8dd05 -r 88131f2807b6 src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Sun Mar 22 20:46:11 2009 +0100
+++ b/src/HOL/Library/Euclidean_Space.thy	Sun Mar 22 20:46:11 2009 +0100
@@ -5,10 +5,10 @@
 header {* (Real) Vectors in Euclidean space, and elementary linear algebra.*}
 
 theory Euclidean_Space
-  imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Complex_Main
+imports Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
   Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type
   Inner_Product
-  uses ("normarith.ML")
+uses ("normarith.ML")
 begin
 
 text{* Some common special cases.*}




