Sun, 13 Sep 2015 22:56:52 +0200 |
wenzelm |
tuned proofs -- less legacy;
|
file |
diff |
annotate
|
Tue, 14 Apr 2015 14:14:43 +0200 |
Andreas Lochbihler |
lemmas about integrals over bind and join on measures
|
file |
diff |
annotate
|
Wed, 08 Apr 2015 21:49:45 +0200 |
wenzelm |
eliminated suspicious Unicode character;
|
file |
diff |
annotate
|
Mon, 23 Mar 2015 10:16:20 +0100 |
hoelzl |
add measurable_submarkov
|
file |
diff |
annotate
|
Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
Thu, 19 Feb 2015 16:32:53 +0100 |
haftmann |
more canonical order of subscriptions avoids superfluous facts
|
file |
diff |
annotate
|
Wed, 11 Feb 2015 15:22:37 +0100 |
Andreas Lochbihler |
more lemmas
|
file |
diff |
annotate
|
Fri, 23 Jan 2015 12:37:23 +0100 |
Andreas Lochbihler |
generalise lemma
|
file |
diff |
annotate
|
Thu, 22 Jan 2015 14:51:08 +0100 |
hoelzl |
import general thms from Density_Compiler
|
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
|
Mon, 24 Nov 2014 12:20:14 +0100 |
hoelzl |
add congruence solver to measurability prover
|
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, 07 Oct 2014 14:02:24 +0200 |
hoelzl |
fix document generation for HOL-Probability
|
file |
diff |
annotate
|
Tue, 07 Oct 2014 10:34:24 +0200 |
hoelzl |
add Giry monad
|
file |
diff |
annotate
|