2012-11-19 hoelzl 2012-11-19 merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
2012-11-16 hoelzl 2012-11-16 renamed measurable_compose -> measurable_finmap_compose, clashed with Sigma_Algebra.measurable_compose
2012-11-16 immler 2012-11-16 allow arbitrary enumerations of basis in locale for generation of borel sets
2012-11-15 immler 2012-11-15 corrected headers
2012-11-15 immler 2012-11-15 added projective limit; proof is based on auxiliary type finmap::polish_space