diff -r a400b06d03cb -r 4cf38ea4fad2 src/HOL/Library/Euclidean_Space.thy --- a/src/HOL/Library/Euclidean_Space.thy Mon Mar 23 07:41:07 2009 +0100 +++ b/src/HOL/Library/Euclidean_Space.thy Mon Mar 23 08:16:24 2009 +0100 @@ -5,7 +5,8 @@ header {* (Real) Vectors in Euclidean space, and elementary linear algebra.*} theory Euclidean_Space -imports Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order" +imports + Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type Inner_Product uses ("normarith.ML")