src/HOL/Probability/Fin_Map.thy
Thu, 04 Dec 2014 17:05:58 +0100 hoelzl generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
Mon, 24 Nov 2014 12:20:14 +0100 hoelzl add congruence solver to measurability prover
Sun, 02 Nov 2014 17:06:05 +0100 wenzelm modernized header;
Wed, 23 Apr 2014 09:32:00 +0200 hoelzl remove add_eq_zero_iff, it is replaced by add_nonneg_eq_0_iff; also removes it from the simpset
Wed, 19 Mar 2014 23:13:45 +0100 wenzelm tuned -- no need for slightly obscure "local" prefix;
Tue, 03 Sep 2013 01:12:40 +0200 wenzelm tuned proofs -- clarified flow of facts wrt. calculation;
Tue, 13 Aug 2013 16:25:47 +0200 wenzelm standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
Tue, 09 Apr 2013 14:04:41 +0200 hoelzl remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
Sat, 23 Mar 2013 20:50:39 +0100 haftmann fundamental revision of big operators on sets
Fri, 22 Mar 2013 10:41:43 +0100 hoelzl move first_countable_topology to the HOL image
Tue, 05 Mar 2013 15:43:14 +0100 hoelzl use generate_topology for second countable topologies, does not require intersection stable basis
Wed, 13 Feb 2013 16:35:07 +0100 immler eliminated union_closed_basis; cleanup Fin_Map
Wed, 13 Feb 2013 16:35:07 +0100 immler fine grained instantiations
Wed, 13 Feb 2013 16:35:07 +0100 immler use maximum norm for type finmap
Mon, 14 Jan 2013 17:29:04 +0100 hoelzl renamed countable_basis_space to second_countable_topology
Wed, 28 Nov 2012 15:38:12 +0100 wenzelm tuned syntax, potentially more robust;
Tue, 27 Nov 2012 13:48:40 +0100 immler based countable topological basis on Countable_Set
Tue, 27 Nov 2012 11:29:47 +0100 immler qualified interpretation of sigma_algebra, to avoid name clashes
Mon, 19 Nov 2012 16:09:11 +0100 hoelzl tuned FinMap
Mon, 19 Nov 2012 12:29:02 +0100 hoelzl merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure
Fri, 16 Nov 2012 14:46:23 +0100 hoelzl renamed measurable_compose -> measurable_finmap_compose, clashed with Sigma_Algebra.measurable_compose
Fri, 16 Nov 2012 11:22:22 +0100 immler allow arbitrary enumerations of basis in locale for generation of borel sets
Thu, 15 Nov 2012 17:36:08 +0100 immler corrected headers
Thu, 15 Nov 2012 11:16:58 +0100 immler added projective limit;
less more (0) tip