20150924 
immler 
20150924 
exchange uniform limit and integral

file  diff  annotate 
20150820 
paulson 
20150820 
The StoneWeierstrass theorem

file  diff  annotate 
20150728 
immler 
20150728 
added theory Uniform_Limit

file  diff  annotate 
20150128 
hoelzl 
20150128 
moved bcontfun from AFP/Ordinary_Differential_Equations

file  diff  annotate 
20140402 
hoelzl 
20140402 
reorder Complex_Analysis_Basics; rename DD to deriv

file  diff  annotate 
20140318 
immler 
20140318 
removed dependencies on theory Ordered_Euclidean_Space

file  diff  annotate 
20121214 
hoelzl 
20121214 
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors

file  diff  annotate 
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 