src/HOL/Library/Euclidean_Space.thy
2009-02-09 chaieb 2009-02-09 fixed proof -- removed unnecessary sorry
2009-02-09 chaieb 2009-02-09 (Real) Vectors in Euclidean space, and elementary linear algebra.