src/HOL/Library/Euclidean_Space.thy
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-03-12 huffman 2009-03-12 remove trailing spaces
2009-03-05 haftmann 2009-03-05 merged
2009-03-05 haftmann 2009-03-05 tuned
2009-03-04 wenzelm 2009-03-04 removed old/broken CVS Ids;
2009-03-04 chaieb 2009-03-04 fixed proofs; added rules as default simp-rules
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.