# HG changeset patch # User hoelzl # Date 1425550302 -3600 # Node ID 304ee0a475d193f3d68ff14192fbabe3111bf116 # Parent 81b33949622cfd5f2de1abf0b8feadec5047f918 fix import path diff -r 81b33949622c -r 304ee0a475d1 src/HOL/Probability/Measure_Space.thy --- 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"