equal
deleted
inserted
replaced
5 Defines the subprobability spaces, the subprobability functor and the Giry monad on subprobability |
5 Defines the subprobability spaces, the subprobability functor and the Giry monad on subprobability |
6 spaces. |
6 spaces. |
7 *) |
7 *) |
8 |
8 |
9 theory Giry_Monad |
9 theory Giry_Monad |
10 imports Probability_Measure "~~/src/HOL/Library/Monad_Syntax" |
10 imports Probability_Measure "HOL-Library.Monad_Syntax" |
11 begin |
11 begin |
12 |
12 |
13 section \<open>Sub-probability spaces\<close> |
13 section \<open>Sub-probability spaces\<close> |
14 |
14 |
15 locale subprob_space = finite_measure + |
15 locale subprob_space = finite_measure + |