| author | hoelzl |
| Mon, 14 Mar 2011 14:37:49 +0100 | |
| changeset 41981 | cdf7693bbe08 |
| parent 41689 | 3e39b0e730d6 |
| child 42147 | 61d5d50ca74c |
| permissions | -rw-r--r-- |
| 33536 | 1 |
theory Probability |
|
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
35833
diff
changeset
|
2 |
imports |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
40859
diff
changeset
|
3 |
Complete_Measure |
|
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset
|
4 |
Lebesgue_Measure |
|
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
35833
diff
changeset
|
5 |
Information |
|
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
35833
diff
changeset
|
6 |
"ex/Dining_Cryptographers" |
|
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
40859
diff
changeset
|
7 |
"ex/Koepf_Duermuth_Countermeasure" |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
8 |
begin |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
9 |
end |