| Wed, 06 Jan 2016 12:18:53 +0100 |
hoelzl |
add the proof of the central limit theorem
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 20:19:59 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
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
|
| 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
|