| Fri, 16 Nov 2012 16:59:56 +0100 |
wenzelm |
made SML/NJ happy;
|
changeset |
files
|
| Fri, 16 Nov 2012 14:46:23 +0100 |
hoelzl |
renamed prob_space to proj_prob_space as it clashed with Probability_Measure.prob_space
|
changeset |
files
|
| Fri, 16 Nov 2012 14:46:23 +0100 |
hoelzl |
renamed measurable_compose -> measurable_finmap_compose, clashed with Sigma_Algebra.measurable_compose
|
changeset |
files
|
| Fri, 16 Nov 2012 14:46:23 +0100 |
hoelzl |
measurability for nat_case and comb_seq
|
changeset |
files
|
| Fri, 16 Nov 2012 14:46:23 +0100 |
hoelzl |
rules for AE and prob
|
changeset |
files
|
| Fri, 16 Nov 2012 14:46:23 +0100 |
hoelzl |
rules for intergration: integrating nat-functions, integrals on finite measures, constant multiplication
|
changeset |
files
|
| Fri, 16 Nov 2012 12:10:02 +0100 |
hoelzl |
more measurability rules
|
changeset |
files
|
| Fri, 16 Nov 2012 11:34:34 +0100 |
immler |
renamed to more appropriate lim_P for projective limit
|
changeset |
files
|
| Fri, 16 Nov 2012 11:22:22 +0100 |
immler |
allow arbitrary enumerations of basis in locale for generation of borel sets
|
changeset |
files
|
| Thu, 15 Nov 2012 17:40:46 +0100 |
haftmann |
repaired slip accidentally introduced in 57209cfbf16b
|
changeset |
files
|
| Thu, 15 Nov 2012 12:11:15 +0100 |
haftmann |
prefer implementation in HOL;
|
changeset |
files
|
| Thu, 15 Nov 2012 17:36:08 +0100 |
immler |
corrected headers
|
changeset |
files
|
| Thu, 15 Nov 2012 16:07:52 +0100 |
immler |
hide constants of auxiliary type finmap
|
changeset |
files
|
| Thu, 15 Nov 2012 15:50:01 +0100 |
immler |
generalized to copy of countable types instead of instantiation of nat for discrete topology
|
changeset |
files
|