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