src/HOL/Library/Euclidean_Space.thy
changeset 30661 54858c8ad226
parent 30582 638b088bb840
child 30665 4cf38ea4fad2
     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Mon Mar 23 08:14:22 2009 +0100
     1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Mon Mar 23 08:14:23 2009 +0100
     1.3 @@ -5,10 +5,10 @@
     1.4  header {* (Real) Vectors in Euclidean space, and elementary linear algebra.*}
     1.5  
     1.6  theory Euclidean_Space
     1.7 -  imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Complex_Main
     1.8 -  Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type
     1.9 -  Inner_Product
    1.10 -  uses ("normarith.ML")
    1.11 +imports
    1.12 +  Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order" 
    1.13 +  Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type Inner_Product
    1.14 +uses ("normarith.ML")
    1.15  begin
    1.16  
    1.17  text{* Some common special cases.*}