src/HOL/Probability/Discrete_Topology.thy

--- a/src/HOL/Probability/Discrete_Topology.thy	Fri Aug 05 18:34:57 2016 +0200
+++ b/src/HOL/Probability/Discrete_Topology.thy	Mon Aug 08 14:13:14 2016 +0200
@@ -3,7 +3,7 @@
 *)
 
 theory Discrete_Topology
-imports "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
+imports "~~/src/HOL/Analysis/Analysis"
 begin
 
 text \<open>Copy of discrete types with discrete topology. This space is polish.\<close>