| Fri, 09 Nov 2012 14:14:45 +0100 |
immler |
removed redundant/unnecessary assumptions from projective_family
|
file |
diff |
annotate
|
| Tue, 06 Nov 2012 11:03:28 +0100 |
immler |
moved lemmas further up
|
file |
diff |
annotate
|
| Tue, 06 Nov 2012 19:18:35 +0100 |
hoelzl |
add support for function application to measurability prover
|
file |
diff |
annotate
|
| Fri, 02 Nov 2012 14:23:54 +0100 |
hoelzl |
use measurability prover
|
file |
diff |
annotate
|
| Fri, 02 Nov 2012 14:00:39 +0100 |
hoelzl |
for the product measure it is enough if only one measure is sigma-finite
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 12:12:23 +0200 |
hoelzl |
remove incseq assumption from measure_eqI_generator_eq
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 12:12:21 +0200 |
hoelzl |
merge should operate on pairs
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 12:12:20 +0200 |
hoelzl |
remove incseq assumption from sigma_prod_algebra_sigma_eq
|
file |
diff |
annotate
|
| Wed, 10 Oct 2012 12:12:18 +0200 |
hoelzl |
tuned product measurability
|
file |
diff |
annotate
|
| Wed, 25 Apr 2012 19:26:00 +0200 |
hoelzl |
moved lemmas to appropriate places
|
file |
diff |
annotate
|
| Mon, 23 Apr 2012 12:14:35 +0200 |
hoelzl |
reworked Probability theory
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 16:56:56 +0100 |
wenzelm |
prefer abs_def over def_raw;
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 13:31:26 +0100 |
wenzelm |
tuned proofs -- eliminated pointless chaining of facts after 'interpret';
|
file |
diff |
annotate
|
| Tue, 28 Feb 2012 21:53:36 +0100 |
wenzelm |
avoid undeclared variables in let bindings;
|
file |
diff |
annotate
|
| Wed, 07 Dec 2011 15:10:29 +0100 |
hoelzl |
remove unnecessary sublocale instantiations in HOL-Probability (for clarity and speedup); remove Infinite_Product_Measure.product_prob_space which was a duplicate of Probability_Measure.product_prob_space
|
file |
diff |
annotate
|
| Wed, 14 Sep 2011 10:08:52 -0400 |
hoelzl |
renamed Complete_Lattices lemmas, removed legacy names
|
file |
diff |
annotate
|
| Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
| Tue, 19 Jul 2011 14:36:12 +0200 |
hoelzl |
Rename extreal => ereal
|
file |
diff |
annotate
|
| Thu, 26 May 2011 17:40:01 +0200 |
hoelzl |
add lemma indep_distribution_eq_measure
|
file |
diff |
annotate
|
| Mon, 23 May 2011 19:21:05 +0200 |
hoelzl |
move lemmas to Extended_Reals and Extended_Real_Limits
|
file |
diff |
annotate
|
| Tue, 29 Mar 2011 14:27:39 +0200 |
hoelzl |
split Product_Measure into Binary_Product_Measure and Finite_Product_Measure
|
file |
diff |
annotate
| base
|