| changeset 63626 | 44ce6b524ff3 |
| parent 63540 | f8652d0534fa |
| child 63886 | 685fb01256af |
--- a/src/HOL/Probability/Giry_Monad.thy Sun Aug 07 12:10:49 2016 +0200 +++ b/src/HOL/Probability/Giry_Monad.thy Fri Aug 05 18:34:57 2016 +0200 @@ -7,7 +7,7 @@ *) theory Giry_Monad - imports Probability_Measure Lebesgue_Integral_Substitution "~~/src/HOL/Library/Monad_Syntax" + imports Probability_Measure "~~/src/HOL/Library/Monad_Syntax" begin section \<open>Sub-probability spaces\<close>