src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy
2011-08-16 huffman 2011-08-16 Multivariate_Analysis includes Determinants.thy, but doesn't import it by default
2011-08-16 huffman 2011-08-16 get Multivariate_Analysis/Determinants.thy compiled and working again
2011-03-14 hoelzl 2011-03-14 split Extended_Reals into parts for Library and Multivariate_Analysis
2011-01-18 hoelzl 2011-01-18 Gauge measure removed
2010-08-23 hoelzl 2010-08-23 Rewrite the Probability theory. Introduced pinfreal as real numbers with infinity. Use pinfreal as value for measures. Introduces Lebesgue Measure based on the integral in Multivariate Analysis. Proved Radon Nikodym for arbitrary sigma finite measure spaces.
2010-06-21 hoelzl 2010-06-21 Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
2010-04-26 huffman 2010-04-26 move proof of Fashoda meet theorem into separate file
2010-02-22 hoelzl 2010-02-22 Replaced Integration by Multivariate-Analysis/Real_Integration
2010-02-17 hoelzl 2010-02-17 Renamed Multivariate-Analysis/Integration to Multivariate-Analysis/Integration_MV to avoid name clash with Integration.
2010-02-17 himmelma 2010-02-17 Added integration to Multivariate-Analysis (upto FTC)
2009-11-17 hoelzl 2009-11-17 Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOL-light)
2009-10-28 wenzelm 2009-10-28 tuned initial session setup;
2009-10-23 himmelma 2009-10-23 distinguished session for multivariate analysis