src/HOL/Probability/Measure_Space.thy
Wed, 07 Oct 2015 17:11:16 +0200 hoelzl cleanup projective limit of probability distributions; proved Ionescu-Tulcea; used it to prove infinite prob. distribution
Sun, 13 Sep 2015 20:20:16 +0200 wenzelm renamed method "goals" to "goal_cases" to emphasize its meaning;
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
Mon, 13 Jul 2015 14:40:16 +0200 hoelzl add emeasure_add_AE
Mon, 13 Jul 2015 14:39:50 +0200 hoelzl stronger induction assumption in lfp_transfer and emeasure_lfp
Fri, 03 Jul 2015 08:26:34 +0200 hoelzl add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
Fri, 26 Jun 2015 10:20:33 +0200 wenzelm tuned whitespace;
Thu, 25 Jun 2015 23:33:47 +0200 wenzelm tuned proofs;
Mon, 04 May 2015 17:35:31 +0200 hoelzl rename continuous and down_continuous in Order_Continuity to sup_/inf_continuous; relate them with topological continuity
Wed, 22 Apr 2015 12:43:06 +0100 paulson fixes for limits
Tue, 21 Apr 2015 17:19:00 +0100 paulson New material, mostly about limits. Consolidation.
Tue, 14 Apr 2015 14:11:01 +0200 Andreas Lochbihler add lemmas about restrict_space
Thu, 05 Mar 2015 11:11:42 +0100 hoelzl fix import path
Thu, 22 Jan 2015 14:51:08 +0100 hoelzl import general thms from Density_Compiler
Mon, 24 Nov 2014 12:20:14 +0100 hoelzl add congruence solver to measurability prover
Mon, 17 Nov 2014 18:19:06 +0100 hoelzl add reindex rules for distr and nn_integral on count_space
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 10:34:24 +0200 hoelzl add Giry monad
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
Mon, 30 Jun 2014 15:45:03 +0200 hoelzl some lemmas about the indicator function; removed lemma sums_def2
Sat, 28 Jun 2014 09:16:42 +0200 haftmann fact consolidation
Wed, 18 Jun 2014 14:31:32 +0200 hoelzl filters are easier to define with INF on filters.
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
Thu, 12 Jun 2014 15:47:36 +0200 hoelzl properties of Erlang and exponentially distributed random variables (by Sudeep Kanav)
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
Tue, 18 Mar 2014 22:11:46 +0100 haftmann consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
less more (0) -30 tip