src/HOL/Library/Euclidean_Space.thy
changeset 30665 4cf38ea4fad2
parent 30655 88131f2807b6
parent 30661 54858c8ad226
child 30960 fec1a04b7220
     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Mon Mar 23 07:41:07 2009 +0100
     1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Mon Mar 23 08:16:24 2009 +0100
     1.3 @@ -5,7 +5,8 @@
     1.4  header {* (Real) Vectors in Euclidean space, and elementary linear algebra.*}
     1.5  
     1.6  theory Euclidean_Space
     1.7 -imports Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
     1.8 +imports
     1.9 +  Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
    1.10    Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type
    1.11    Inner_Product
    1.12  uses ("normarith.ML")