fix import path
authorhoelzl
Thu, 05 Mar 2015 11:11:42 +0100
changeset 59593 304ee0a475d1
parent 59592 81b33949622c
child 59594 43f0c669302d
child 59613 7103019278f0
child 59616 eb59c6968219
fix import path
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"