src/HOL/Probability/Sigma_Algebra.thy
Tue, 23 Feb 2016 16:25:08 +0100 nipkow more canonical names
Wed, 17 Feb 2016 21:51:56 +0100 haftmann prefer abbreviations for compound operators INFIMUM and SUPREMUM
Wed, 06 Jan 2016 12:18:53 +0100 hoelzl add the proof of the central limit theorem
Mon, 28 Dec 2015 17:43:30 +0100 wenzelm prefer symbols for "Union", "Inter";
Wed, 25 Nov 2015 22:44:02 +0100 hoelzl infix syntax for measurable set
Mon, 07 Dec 2015 20:19:59 +0100 wenzelm isabelle update_cartouches -c -t;
Wed, 11 Nov 2015 10:13:40 +0100 Andreas Lochbihler add lemmas
Tue, 10 Nov 2015 14:43:29 +0000 paulson Merge
Tue, 10 Nov 2015 14:18:41 +0000 paulson Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
Mon, 09 Nov 2015 15:48:17 +0100 wenzelm qualifier is mandatory by default;
Sat, 10 Oct 2015 19:22:05 +0200 wenzelm prefer symbols;
Sun, 13 Sep 2015 22:56:52 +0200 wenzelm tuned proofs -- less legacy;
Thu, 23 Jul 2015 16:40:47 +0200 hoelzl Measures form a CCPO
Thu, 16 Jul 2015 10:48:20 +0200 hoelzl move disjoint sets to their own theory
Tue, 14 Apr 2015 14:11:01 +0200 Andreas Lochbihler add lemmas about restrict_space
Fri, 16 Jan 2015 10:59:15 +0100 hoelzl tuned measurability proofs
Thu, 15 Jan 2015 15:04:51 +0100 hoelzl piecewise measurability using restrict_space; cleanup Borel_Space
Fri, 05 Dec 2014 12:06:18 +0100 hoelzl add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
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
Thu, 13 Nov 2014 17:19:52 +0100 hoelzl import general theorems from AFP/Markov_Models
Sun, 02 Nov 2014 17:06:05 +0100 wenzelm modernized header;
Tue, 07 Oct 2014 14:02:24 +0200 hoelzl fix document generation for HOL-Probability
Tue, 07 Oct 2014 10:34:24 +0200 hoelzl add Giry monad
Mon, 06 Oct 2014 16:27:31 +0200 hoelzl add measure space for (coinductive) streams
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
Mon, 30 Jun 2014 15:45:21 +0200 hoelzl import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
Sat, 28 Jun 2014 09:16:42 +0200 haftmann fact consolidation
Wed, 18 Jun 2014 07:31:12 +0200 hoelzl moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
Fri, 30 May 2014 18:48:05 +0200 hoelzl generalizd measurability on restricted space; rule for integrability on compact sets
Fri, 30 May 2014 15:56:30 +0200 hoelzl better support for restrict_space
Tue, 20 May 2014 19:24:39 +0200 hoelzl add various lemmas
Mon, 19 May 2014 13:44:13 +0200 hoelzl fixed document generation for HOL-Probability
Mon, 19 May 2014 12:04:45 +0200 hoelzl introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
Tue, 13 May 2014 11:35:47 +0200 hoelzl clean up Lebesgue integration
Sat, 15 Mar 2014 08:31:33 +0100 haftmann more complete set of lemmas wrt. image and composition
Wed, 13 Nov 2013 09:37:00 +0100 hoelzl fix document generation for HOL-Probability
Tue, 12 Nov 2013 19:28:56 +0100 hoelzl measure of a countable union
Tue, 12 Nov 2013 19:28:56 +0100 hoelzl add restrict_space measure
Tue, 24 Sep 2013 10:35:37 +0200 Andreas Lochbihler make measure_of total
Tue, 03 Sep 2013 01:12:40 +0200 wenzelm tuned proofs -- clarified flow of facts wrt. calculation;
Wed, 10 Apr 2013 18:51:21 +0200 hoelzl generalize Borel-set properties from real/ereal/ordered_euclidean_spaces to order_topology and real_normed_vector
Fri, 14 Dec 2012 15:46:01 +0100 hoelzl Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
Wed, 05 Dec 2012 15:59:08 +0100 hoelzl Move the measurability prover to its own file
Wed, 05 Dec 2012 15:58:48 +0100 hoelzl Show search depth in the debug output of the measurability prover
Thu, 29 Nov 2012 09:59:20 +0100 hoelzl make SML/NJ happy (give names for all fields in a record)
Wed, 28 Nov 2012 15:59:18 +0100 wenzelm eliminated slightly odd identifiers;
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
Fri, 16 Nov 2012 12:10:02 +0100 hoelzl more measurability rules
Tue, 06 Nov 2012 19:18:35 +0100 hoelzl add support for function application to measurability prover
Fri, 02 Nov 2012 14:23:54 +0100 hoelzl use measurability prover
Fri, 02 Nov 2012 14:23:40 +0100 hoelzl add measurability prover; add support for Borel sets
Fri, 12 Oct 2012 18:58:20 +0200 wenzelm discontinued obsolete typedef (open) syntax;
Wed, 10 Oct 2012 12:12:27 +0200 hoelzl add induction rule for intersection-stable sigma-sets
Wed, 10 Oct 2012 12:12:22 +0200 hoelzl add measurable_compose
Wed, 10 Oct 2012 12:12:15 +0200 hoelzl tuned measurable_If; moved countably_additive equalities to Measure_Space; tuned proofs
Wed, 25 Apr 2012 19:26:27 +0200 hoelzl add Caratheodories theorem for semi-rings of sets
Wed, 25 Apr 2012 15:06:59 +0200 hoelzl correct lemma name
Mon, 23 Apr 2012 12:14:35 +0200 hoelzl reworked Probability theory
less more (0) -60 tip