src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy
Fri, 14 Dec 2012 15:46:01 +0100 hoelzl Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
Tue, 16 Aug 2011 13:07:52 -0700 huffman Multivariate_Analysis includes Determinants.thy, but doesn't import it by default
Tue, 16 Aug 2011 07:56:17 -0700 huffman get Multivariate_Analysis/Determinants.thy compiled and working again
less more (0) -10 -3 tip