20110816 
huffman 
20110816 
Multivariate_Analysis includes Determinants.thy, but doesn't import it by default

file  diff  annotate 
20110816 
huffman 
20110816 
get Multivariate_Analysis/Determinants.thy compiled and working again

file  diff  annotate 
20110314 
hoelzl 
20110314 
split Extended_Reals into parts for Library and Multivariate_Analysis

file  diff  annotate 
20110118 
hoelzl 
20110118 
Gauge measure removed

file  diff  annotate 
20100823 
hoelzl 
20100823 
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.

file  diff  annotate 
20100621 
hoelzl 
20100621 
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.

file  diff  annotate 
20100426 
huffman 
20100426 
move proof of Fashoda meet theorem into separate file

file  diff  annotate 
20100222 
hoelzl 
20100222 
Replaced Integration by MultivariateAnalysis/Real_Integration

file  diff  annotate 
20100217 
hoelzl 
20100217 
Renamed MultivariateAnalysis/Integration to MultivariateAnalysis/Integration_MV to avoid name clash with Integration.

file  diff  annotate 
20100217 
himmelma 
20100217 
Added integration to MultivariateAnalysis (upto FTC)

file  diff  annotate 
20091117 
hoelzl 
20091117 
Added derivation and Brouwer's fixpoint theorem in Multivariate Analysis (translated by Robert Himmelmann from HOLlight)

file  diff  annotate 
20091028 
wenzelm 
20091028 
tuned initial session setup;

file  diff  annotate 
20091023 
himmelma 
20091023 
distinguished session for multivariate analysis

file  diff  annotate 