| 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
|