src/HOL/Library/Euclidean_Space.thy
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-02-22 huffman 2009-02-22 remove duplicate instance declaration
2009-02-21 huffman 2009-02-21 real_inner class instance for vectors
2009-02-21 huffman 2009-02-21 remove duplicated lemmas about norm
2009-02-21 huffman 2009-02-21 real_normed_vector instance
2009-02-21 huffman 2009-02-21 fix real_vector, real_algebra instances
2009-02-13 huffman 2009-02-13 section -> subsection
2009-02-13 huffman 2009-02-13 add instance for cancel_comm_monoid_add
2009-02-12 huffman 2009-02-12 fix document generation
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.