src/HOL/Probability/Probability_Mass_Function.thy
2016-06-22 wenzelm 2016-06-22 bundle lifting_syntax;
2016-05-31 eberlm 2016-05-31 Added code generation for PMFs
2016-05-18 Manuel Eberl 2016-05-18 Resolved name clash
2016-05-17 eberlm 2016-05-17 Moved material from AFP/Randomised_Social_Choice to distribution
2016-05-13 wenzelm 2016-05-13 eliminated use of empty "assms";
2016-04-25 wenzelm 2016-04-25 eliminated old 'def'; tuned comments;
2016-04-14 hoelzl 2016-04-14 Probability: move emeasure and nn_integral from ereal to ennreal
2016-02-23 nipkow 2016-02-23 more canonical names
2016-02-16 traytel 2016-02-16 make predicator a first-class bnf citizen
2016-01-06 hoelzl 2016-01-06 add the proof of the central limit theorem
2016-01-01 wenzelm 2016-01-01 more symbols;
2015-12-07 wenzelm 2015-12-07 isabelle update_cartouches -c -t;
2015-11-11 Andreas Lochbihler 2015-11-11 add various lemmas
2015-11-10 paulson 2015-11-10 Merge
2015-11-10 paulson 2015-11-10 Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
2015-11-09 wenzelm 2015-11-09 qualifier is mandatory by default;
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-09-13 wenzelm 2015-09-13 tuned proofs -- less legacy;
2015-06-17 hoelzl 2015-06-17 generalized geometric distribution
2015-06-27 wenzelm 2015-06-27 premises in 'show' are treated like 'assume';
2015-06-17 nipkow 2015-06-17 renamed Multiset.set_of to the canonical set_mset
2015-04-14 Andreas Lochbihler 2015-04-14 add various lemmas about pmfs
2015-03-17 paulson 2015-03-17 Merge
2015-03-16 paulson 2015-03-16 The factorial function, "fact", now has type "nat => 'a"
2015-03-12 hoelzl 2015-03-12 rel_pmf on equivalence relation
2015-03-10 hoelzl 2015-03-10 generalized bind_cond_pmf_cancel
2015-03-10 paulson 2015-03-10 Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
2015-03-10 hoelzl 2015-03-10 add set_pmf lemmas to simpset
2015-03-10 hoelzl 2015-03-10 build pmf's on bind
2015-02-19 haftmann 2015-02-19 establish unique preferred fact names
2015-02-11 Andreas Lochbihler 2015-02-11 rel_pmf preserves orders
2015-02-11 Andreas Lochbihler 2015-02-11 generalise lemma
2015-02-11 Andreas Lochbihler 2015-02-11 more lemmas
2015-02-10 hoelzl 2015-02-10 merged
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