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