20130305 
hoelzl 
20130305 
generalized lemmas in Extended_Real_Limits

file  diff  annotate 
20130131 
hoelzl 
20130131 
use order topology for extended reals

file  diff  annotate 
20121207 
hoelzl 
20121207 
add exponential and uniform distributions

file  diff  annotate 
20121205 
hoelzl 
20121205 
Move the measurability prover to its own file

file  diff  annotate 
20121127 
immler 
20121127 
qualified interpretation of sigma_algebra, to avoid name clashes

file  diff  annotate 
20121116 
hoelzl 
20121116 
move theorems to be more generally useable

file  diff  annotate 
20121115 
immler 
20121115 
regularity of measures, therefore:
characterization of closure with infimum distance;
characterize of compact sets as totally bounded;
added Diagonal_Subsequence to Library;
introduced (enumerable) topological basis;
rational boxes as basis of ordered euclidean space;
moved some lemmas upwards

file  diff  annotate 
20121102 
hoelzl 
20121102 
add measurability prover; add support for Borel sets

file  diff  annotate 
20121102 
hoelzl 
20121102 
add syntax and a.e.rules for (conditional) probability on predicates

file  diff  annotate 
20121010 
hoelzl 
20121010 
add induction rule for intersectionstable sigmasets

file  diff  annotate 
20121010 
hoelzl 
20121010 
remove incseq assumption from measure_eqI_generator_eq

file  diff  annotate 
20121010 
hoelzl 
20121010 
tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs

file  diff  annotate 
20120425 
hoelzl 
20120425 
add Caratheodories theorem for semirings of sets

file  diff  annotate 
20120425 
hoelzl 
20120425 
moved lemmas to appropriate places

file  diff  annotate 
20120423 
hoelzl 
20120423 
reworked Probability theory

file  diff  annotate 