src/HOL/Library/Product_Vector.thy
Fri, 20 Feb 2009 08:02:11 -0800 huffman add theory of products as real vector spaces to Library
less more (0) tip