--- a/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy	Sun Aug 07 12:10:49 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Multivariate_Analysis.thy	Fri Aug 05 18:34:57 2016 +0200
@@ -1,10 +1,13 @@
 theory Multivariate_Analysis
 imports
+  Regularity
+  Lebesgue_Integral_Substitution
+  Embed_Measure
+  Complete_Measure
+  Radon_Nikodym
   Fashoda_Theorem
-  Extended_Real_Limits
   Determinants
   Homeomorphism
-  Ordered_Euclidean_Space
   Bounded_Continuous_Function
   Weierstrass_Theorems
   Polytope