1.1 --- a/src/HOL/Probability/Discrete_Topology.thy	Thu Jan 31 11:31:27 2013 +0100
     1.2 +++ b/src/HOL/Probability/Discrete_Topology.thy	Thu Jan 31 11:31:30 2013 +0100
     1.3 @@ -3,7 +3,7 @@
     1.4  *)
     1.5  
     1.6  theory Discrete_Topology
     1.7 -imports Multivariate_Analysis
     1.8 +imports "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
     1.9  begin
    1.10  
    1.11  text {* Copy of discrete types with discrete topology. This space is polish. *}