src/HOL/Probability/Fin_Map.thy
2013-04-09 hoelzl 2013-04-09 remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
2013-03-23 haftmann 2013-03-23 fundamental revision of big operators on sets
2013-03-22 hoelzl 2013-03-22 move first_countable_topology to the HOL image
2013-03-05 hoelzl 2013-03-05 use generate_topology for second countable topologies, does not require intersection stable basis
2013-02-13 immler 2013-02-13 eliminated union_closed_basis; cleanup Fin_Map
2013-02-13 immler 2013-02-13 fine grained instantiations
2013-02-13 immler 2013-02-13 use maximum norm for type finmap
2013-01-14 hoelzl 2013-01-14 renamed countable_basis_space to second_countable_topology
2012-11-28 wenzelm 2012-11-28 tuned syntax, potentially more robust;
2012-11-27 immler 2012-11-27 based countable topological basis on Countable_Set
2012-11-27 immler 2012-11-27 qualified interpretation of sigma_algebra, to avoid name clashes
2012-11-19 hoelzl 2012-11-19 tuned FinMap
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