equal
deleted
inserted
replaced
|
1 (* Title: HOL/Probability/Probability.thy |
|
2 Author: Johannes Hölzl, TU München |
|
3 *) |
|
4 |
1 theory Probability |
5 theory Probability |
2 imports |
6 imports |
3 Discrete_Topology |
7 Discrete_Topology |
4 Complete_Measure |
8 Complete_Measure |
5 Projective_Limit |
9 Projective_Limit |
6 Independent_Family |
10 Independent_Family |
7 Distributions |
11 Distributions |
8 Probability_Mass_Function |
12 Probability_Mass_Function |
9 Stream_Space |
13 Stream_Space |
|
14 Embed_Measure |
|
15 Interval_Integral |
|
16 Set_Integral |
10 Giry_Monad |
17 Giry_Monad |
11 begin |
18 begin |
12 |
19 |
13 end |
20 end |