# HG changeset patch
# User hoelzl
# Date 1478279910 -3600
# Node ID 96b56c98f346f972b7a54385950cf9a3130d194b
# Parent  be149db8207a36f0f22f1b4f9d7b1fa479397747
HOL-Probability: fix import path in Fin_Map

diff -r be149db8207a -r 96b56c98f346 src/HOL/Probability/Fin_Map.thy
--- a/src/HOL/Probability/Fin_Map.thy	Fri Nov 04 15:22:12 2016 +0100
+++ b/src/HOL/Probability/Fin_Map.thy	Fri Nov 04 18:18:30 2016 +0100
@@ -5,7 +5,7 @@
 section \<open>Finite Maps\<close>
 
 theory Fin_Map
-  imports Finite_Product_Measure "~~/src/HOL/Library/Finite_Map"
+  imports "~~/src/HOL/Analysis/Finite_Product_Measure" "~~/src/HOL/Library/Finite_Map"
 begin
 
 text \<open>The @{type fmap} type can be instantiated to @{class polish_space}, needed for the proof of