src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy
2016-01-04 eberlm 2016-01-04 Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
2015-10-26 paulson 2015-10-26 new lemmas about topology, etc., for Cauchy integral formula
2015-09-24 immler 2015-09-24 exchange uniform limit and integral
2015-08-20 paulson 2015-08-20 The Stone-Weierstrass theorem
2015-07-28 immler 2015-07-28 added theory Uniform_Limit
2015-01-28 hoelzl 2015-01-28 moved bcontfun from AFP/Ordinary_Differential_Equations
2014-04-02 hoelzl 2014-04-02 reorder Complex_Analysis_Basics; rename DD to deriv
2014-03-18 immler 2014-03-18 removed dependencies on theory Ordered_Euclidean_Space
2012-12-14 hoelzl 2012-12-14 Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
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