# 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"