src/HOL/Library/Product_Vector.thy
2009-05-28 huffman 2009-05-28 define dist for products
2009-03-26 wenzelm 2009-03-26 interpretation/interpret: prefixes are mandatory by default;
2009-02-20 huffman 2009-02-20 add theory of products as real vector spaces to Library