src/HOL/Library/Euclidean_Space.thy
changeset 30665 4cf38ea4fad2
parent 30655 88131f2807b6
parent 30661 54858c8ad226
child 30960 fec1a04b7220
equal deleted inserted replaced
30659:a400b06d03cb 30665:4cf38ea4fad2
     3 *)
     3 *)
     4 
     4 
     5 header {* (Real) Vectors in Euclidean space, and elementary linear algebra.*}
     5 header {* (Real) Vectors in Euclidean space, and elementary linear algebra.*}
     6 
     6 
     7 theory Euclidean_Space
     7 theory Euclidean_Space
     8 imports Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
     8 imports
       
     9   Complex_Main "~~/src/HOL/Decision_Procs/Dense_Linear_Order"
     9   Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type
    10   Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type
    10   Inner_Product
    11   Inner_Product
    11 uses ("normarith.ML")
    12 uses ("normarith.ML")
    12 begin
    13 begin
    13 
    14