# HG changeset patch
# User haftmann
# Date 1237751171 -3600
# Node ID 88131f2807b6c857e557df8137eb0883c9d2de5b
# Parent  254478a8dd05b88ca48bb236fb5e93f0b982457d
tuned header

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.*}