20140630 
hoelzl 
20140630 
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure

file  diff  annotate 
20140628 
haftmann 
20140628 
fact consolidation

file  diff  annotate 
20130813 
wenzelm 
20130813 
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;

file  diff  annotate 
20121128 
wenzelm 
20121128 
eliminated slightly odd identifiers;

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

file  diff  annotate 
20121119 
hoelzl 
20121119 
tuned FinMap

file  diff  annotate 
20121119 
hoelzl 
20121119 
merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure

file  diff  annotate 
20121116 
hoelzl 
20121116 
renamed prob_space to proj_prob_space as it clashed with Probability_Measure.prob_space

file  diff  annotate 
20121116 
immler 
20121116 
renamed to more appropriate lim_P for projective limit

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 
20121109 
immler 
20121109 
moved lemmas into projective_family; added header for theory Projective_Family

file  diff  annotate 
20121109 
immler 
20121109 
removed redundant/unnecessary assumptions from projective_family

file  diff  annotate 
20121107 
immler 
20121107 
assume probability spaces; allow empty index set

file  diff  annotate 
20121107 
immler 
20121107 
added projective_family; generalized generator in product_prob_space to projective_family

file  diff  annotate 