tuned header
authorhaftmann
Sun Mar 22 20:46:11 2009 +0100 (2009-03-22)
changeset 3065588131f2807b6
parent 30654 254478a8dd05
child 30656 ddb1fafa2dcb
tuned header
src/HOL/Library/Euclidean_Space.thy
     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Sun Mar 22 20:46:11 2009 +0100
     1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Sun Mar 22 20:46:11 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 +imports Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
     1.9    Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type
    1.10    Inner_Product
    1.11 -  uses ("normarith.ML")
    1.12 +uses ("normarith.ML")
    1.13  begin
    1.14  
    1.15  text{* Some common special cases.*}