src/HOL/Probability/Probability_Mass_Function.thy
2015-02-10 hoelzl 2015-02-10 add bind_cond_pmf_cancel
2015-02-10 hoelzl 2015-02-10 add cond_map_pmf
2015-02-10 hoelzl 2015-02-10 introduce discrete conditional probabilities, use it to simplify bnf proof of pmf
2015-02-10 Andreas Lochbihler 2015-02-10 tuned proof
2015-02-10 Andreas Lochbihler 2015-02-10 tune proof
2015-01-30 hoelzl 2015-01-30 simp rules for return_pmf
2015-01-22 hoelzl 2015-01-22 import general thms from Density_Compiler
2015-01-09 hoelzl 2015-01-09 rel_pmf OO: conversion to nat is not necessary
2015-01-09 Andreas Lochbihler 2015-01-09 simplify construction for distribution of rel_pmf over op OO
2014-12-12 hoelzl 2014-12-12 rel_pmf commutes with rel_prod
2014-12-05 hoelzl 2014-12-05 add Poisson and Binomial distribution
2014-12-05 hoelzl 2014-12-05 add integral substitution theorems from Manuel Eberl, Jeremy Avigad, Luke Serafin, and Sudeep Kanav
2014-11-25 hoelzl 2014-11-25 tuned proof that pmfs are bnfs
2014-11-25 hoelzl 2014-11-25 projections of pair_pmf (by D. Traytel)
2014-11-24 hoelzl 2014-11-24 add congruence solver to measurability prover
2014-11-21 Andreas Lochbihler 2014-11-21 add lemma
2014-11-21 Andreas Lochbihler 2014-11-21 register pmf as BNF
2014-11-14 hoelzl 2014-11-14 cleaning up some theorem names; remove unnecessary assumptions; more complete pmf theory
2014-11-13 hoelzl 2014-11-13 import general theorems from AFP/Markov_Models
2014-10-21 hoelzl 2014-10-21 add transfer rule for set_pmf
2014-10-07 hoelzl 2014-10-07 add Giry monad
2014-10-06 hoelzl 2014-10-06 add type for probability mass functions, i.e. discrete probability distribution