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 measurable_compose > measurable_finmap_compose, clashed with Sigma_Algebra.measurable_compose

file  diff  annotate 
20121116 
immler 
20121116 
allow arbitrary enumerations of basis in locale for generation of borel sets

file  diff  annotate 
20121115 
immler 
20121115 
corrected headers

file  diff  annotate 
20121115 
immler 
20121115 
added projective limit;
proof is based on auxiliary type finmap::polish_space

file  diff  annotate 