author | hoelzl |
Thu, 05 Mar 2015 11:11:42 +0100 | |
changeset 59593 | 304ee0a475d1 |
parent 59592 | 81b33949622c |
child 59594 | 43f0c669302d |
child 59613 | 7103019278f0 |
child 59616 | eb59c6968219 |
--- a/src/HOL/Probability/Measure_Space.thy Wed Mar 04 23:42:47 2015 +0100 +++ b/src/HOL/Probability/Measure_Space.thy Thu Mar 05 11:11:42 2015 +0100 @@ -8,7 +8,7 @@ theory Measure_Space imports - Measurable Multivariate_Analysis + Measurable "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis" begin subsection "Relate extended reals and the indicator function"