| Wed, 04 Nov 2015 08:13:49 +0100 |
ballarin |
Qualifiers in locale expressions default to mandatory regardless of the command.
|
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
|
| Thu, 16 Jul 2015 10:48:20 +0200 |
hoelzl |
move disjoint sets to their own theory
|
file |
diff |
annotate
|
| Tue, 14 Apr 2015 14:13:51 +0200 |
Andreas Lochbihler |
add lemmas
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 12:17:22 +0100 |
Andreas Lochbihler |
add another lemma to split nn_integral over product count_space
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 12:05:21 +0100 |
Andreas Lochbihler |
nn_integral can be split over arbitrary product count_spaces
|
file |
diff |
annotate
|
| Fri, 23 Jan 2015 12:04:27 +0100 |
hoelzl |
integral of the product of count spaces equals the integral of the count space of the product type
|
file |
diff |
annotate
|
| Tue, 13 Jan 2015 19:10:36 +0100 |
hoelzl |
measurability prover: removed app splitting, replaced by more powerful destruction rules
|
file |
diff |
annotate
|
| Thu, 04 Dec 2014 17:05:58 +0100 |
hoelzl |
generalized (borel_)measurable_SUP/INF/lfp/gfp; tuned proofs for sigma-closure of product spaces
|
file |
diff |
annotate
|
| Mon, 24 Nov 2014 12:20:14 +0100 |
hoelzl |
add congruence solver to measurability prover
|
file |
diff |
annotate
|
| Thu, 13 Nov 2014 17:19:52 +0100 |
hoelzl |
import general theorems from AFP/Markov_Models
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 17:06:05 +0100 |
wenzelm |
modernized header;
|
file |
diff |
annotate
|
| Tue, 07 Oct 2014 10:34:24 +0200 |
hoelzl |
add Giry monad
|
file |
diff |
annotate
|
| Mon, 30 Jun 2014 15:45:21 +0200 |
hoelzl |
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
|
file |
diff |
annotate
|