src/HOL/Probability/Fin_Map.thy
2016-01-08 hoelzl 2016-01-08 add uniform spaces
2015-12-30 wenzelm 2015-12-30 clarified print modes;
2015-12-30 wenzelm 2015-12-30 more symbols;
2015-12-29 wenzelm 2015-12-29 more symbols;
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-10-09 wenzelm 2015-10-09 discontinued specific HTML syntax;
2014-12-04 hoelzl 2014-12-04 generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
2014-11-24 hoelzl 2014-11-24 add congruence solver to measurability prover
2014-11-02 wenzelm 2014-11-02 modernized header;
2014-04-23 hoelzl 2014-04-23 remove add_eq_zero_iff, it is replaced by add_nonneg_eq_0_iff; also removes it from the simpset
2014-03-19 wenzelm 2014-03-19 tuned -- no need for slightly obscure "local" prefix;
2013-09-03 wenzelm 2013-09-03 tuned proofs -- clarified flow of facts wrt. calculation;
2013-08-13 wenzelm 2013-08-13 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
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