src/HOL/Probability/Fin_Map.thy
8 months ago haftmann 2018-11-18 removed legacy input syntax
8 months ago haftmann 2018-11-08 removed relics of ASCII syntax for indexed big operators
14 months ago paulson 2018-05-08 one tiny fix
18 months ago nipkow 2018-01-10 ran isabelle update_op on all sources
23 months ago wenzelm 2017-08-18 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
2017-07-11 Lars Hupel 2017-07-11 fmaps are countable
2017-07-10 Lars Hupel 2017-07-10 finite sets are countable
2017-06-15 paulson 2017-06-15 Some new material. SIMPRULE STATUS for sum/prod.delta rules!
2016-11-04 hoelzl 2016-11-04 HOL-Probability: fix import path in Fin_Map
2016-09-15 Lars Hupel 2016-09-15 new type for finite maps; use it in HOL-Probability
2016-08-02 immler 2016-08-02 more natural definition of type finmap
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-02-23 nipkow 2016-02-23 more canonical names
2016-02-17 haftmann 2016-02-17 prefer abbreviations for compound operators INFIMUM and SUPREMUM
2016-01-08 hoelzl 2016-01-08 fix code generation for uniformity: uniformity is a non-computable pure data.
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