src/HOL/Probability/Probability_Mass_Function.thy
Tue, 23 Feb 2016 16:25:08 +0100 nipkow more canonical names
Tue, 16 Feb 2016 22:28:19 +0100 traytel make predicator a first-class bnf citizen
Wed, 06 Jan 2016 12:18:53 +0100 hoelzl add the proof of the central limit theorem
Fri, 01 Jan 2016 14:44:52 +0100 wenzelm more symbols;
Mon, 07 Dec 2015 20:19:59 +0100 wenzelm isabelle update_cartouches -c -t;
Wed, 11 Nov 2015 10:28:22 +0100 Andreas Lochbihler add various 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;
Tue, 13 Oct 2015 09:21:15 +0200 haftmann prod_case as canonical name for product type eliminator
Sun, 13 Sep 2015 22:56:52 +0200 wenzelm tuned proofs -- less legacy;
Wed, 17 Jun 2015 18:44:23 +0200 hoelzl generalized geometric distribution
Sat, 27 Jun 2015 00:10:24 +0200 wenzelm premises in 'show' are treated like 'assume';
Wed, 17 Jun 2015 17:21:11 +0200 nipkow renamed Multiset.set_of to the canonical set_mset
Tue, 14 Apr 2015 14:15:10 +0200 Andreas Lochbihler add various lemmas about pmfs
Tue, 17 Mar 2015 12:23:56 +0000 paulson Merge
Mon, 16 Mar 2015 15:30:00 +0000 paulson The factorial function, "fact", now has type "nat => 'a"
Thu, 12 Mar 2015 19:09:18 +0100 hoelzl rel_pmf on equivalence relation
Tue, 10 Mar 2015 17:50:10 +0100 hoelzl generalized bind_cond_pmf_cancel
Tue, 10 Mar 2015 15:20:40 +0000 paulson Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
Tue, 10 Mar 2015 11:56:32 +0100 hoelzl add set_pmf lemmas to simpset
Tue, 10 Mar 2015 10:53:48 +0100 hoelzl build pmf's on bind
Thu, 19 Feb 2015 11:53:36 +0100 haftmann establish unique preferred fact names
Wed, 11 Feb 2015 18:39:56 +0100 Andreas Lochbihler rel_pmf preserves orders
Wed, 11 Feb 2015 18:38:34 +0100 Andreas Lochbihler generalise lemma
Wed, 11 Feb 2015 15:22:37 +0100 Andreas Lochbihler more lemmas
Tue, 10 Feb 2015 14:06:57 +0100 hoelzl merged
Tue, 10 Feb 2015 13:50:30 +0100 hoelzl add bind_cond_pmf_cancel
Tue, 10 Feb 2015 12:15:05 +0100 hoelzl add cond_map_pmf
Tue, 10 Feb 2015 12:09:32 +0100 hoelzl introduce discrete conditional probabilities, use it to simplify bnf proof of pmf
Tue, 10 Feb 2015 12:27:30 +0100 Andreas Lochbihler tuned proof
Tue, 10 Feb 2015 12:10:26 +0100 Andreas Lochbihler tune proof
Fri, 30 Jan 2015 17:29:51 +0100 hoelzl simp rules for return_pmf
Thu, 22 Jan 2015 14:51:08 +0100 hoelzl import general thms from Density_Compiler
Fri, 09 Jan 2015 10:49:35 +0100 hoelzl rel_pmf OO: conversion to nat is not necessary
Fri, 09 Jan 2015 09:16:51 +0100 Andreas Lochbihler simplify construction for distribution of rel_pmf over op OO
Fri, 12 Dec 2014 10:58:40 +0100 hoelzl rel_pmf commutes with rel_prod
Fri, 05 Dec 2014 13:39:59 +0100 hoelzl add Poisson and Binomial distribution
Fri, 05 Dec 2014 12:06:18 +0100 hoelzl add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
Tue, 25 Nov 2014 17:30:05 +0100 hoelzl tuned proof that pmfs are bnfs
Tue, 25 Nov 2014 17:29:39 +0100 hoelzl projections of pair_pmf (by D. Traytel)
Mon, 24 Nov 2014 12:20:14 +0100 hoelzl add congruence solver to measurability prover
Fri, 21 Nov 2014 12:24:59 +0100 Andreas Lochbihler add lemma
Fri, 21 Nov 2014 12:11:44 +0100 Andreas Lochbihler register pmf as BNF
Fri, 14 Nov 2014 13:18:33 +0100 hoelzl cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
Thu, 13 Nov 2014 17:19:52 +0100 hoelzl import general theorems from AFP/Markov_Models
Tue, 21 Oct 2014 17:00:42 +0200 hoelzl add transfer rule for set_pmf
Tue, 07 Oct 2014 10:34:24 +0200 hoelzl add Giry monad
Mon, 06 Oct 2014 16:27:07 +0200 hoelzl add type for probability mass functions, i.e. discrete probability distribution
less more (0) tip