src/HOL/Probability/Probability_Mass_Function.thy
20 months ago haftmann 2017-10-08 avoid name clashes on interpretation of abstract locales
22 months ago eberlm 2017-08-31 Connecting PMFs to infinite sums
22 months ago wenzelm 2017-08-18 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
2017-06-26 paulson 2017-06-26 A few renamings and several tidied-up proofs
2017-06-15 paulson 2017-06-15 Some new material. SIMPRULE STATUS for sum/prod.delta rules!
2017-04-04 eberlm 2017-04-04 moved material from AFP to distribution
2016-12-22 haftmann 2016-12-22 proper logical constants
2016-10-17 nipkow 2016-10-17 setsum -> sum
2016-09-30 hoelzl 2016-09-30 HOL-Probability: more about probability, prepare for Markov processes in the AFP
2016-09-30 hoelzl 2016-09-30 Probability: fix proof
2016-09-19 fleury 2016-09-19 left_distrib ~> distrib_right, right_distrib ~> distrib_left
2016-09-16 hoelzl 2016-09-16 move Henstock-Kurzweil integration after Lebesgue_Measure; replace content by abbreviation measure lborel
2016-09-15 nipkow 2016-09-15 renamed listsum -> sum_list, listprod ~> prod_list
2016-08-12 wenzelm 2016-08-12 more symbols;
2016-07-22 wenzelm 2016-07-22 tuned proofs -- avoid unstructured calculation;
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