src/HOL/Multivariate_Analysis/Linear_Algebra.thy
Fri, 12 Aug 2011 20:55:22 -0700 huffman remove redundant lemma setsum_norm in favor of norm_setsum;
Fri, 12 Aug 2011 09:17:24 -0700 huffman make Multivariate_Analysis work with separate set type
Thu, 11 Aug 2011 13:05:56 -0700 huffman modify euclidean_space class to include basis set
Wed, 10 Aug 2011 18:02:16 -0700 huffman avoid warnings about duplicate rules
Wed, 10 Aug 2011 09:23:42 -0700 huffman split Linear_Algebra.thy from Euclidean_Space.thy
less more (0) tip