author | hoelzl |
Tue, 29 Mar 2011 14:27:42 +0200 | |
changeset 42148 | d596e7bb251f |
parent 42147 | 61d5d50ca74c |
child 42861 | 16375b493b64 |
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 |
42148 | 5 |
Probability_Measure |
42147 | 6 |
Infinite_Product_Measure |
36080
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
35833
diff
changeset
|
7 |
Information |
0d9affa4e73c
Added Information theory and Example: dining cryptographers
hoelzl
parents:
35833
diff
changeset
|
8 |
"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
|
9 |
"ex/Koepf_Duermuth_Countermeasure" |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
10 |
begin |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
11 |
end |