Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
HOL-Probability: fix import path in Fin_Map
authorhoelzl
Fri, 04 Nov 2016 18:18:30 +0100
changeset 64462 96b56c98f346
parent 64461 be149db8207a
child 64463 bed02fca80b5
HOL-Probability: fix import path in Fin_Map
src/HOL/Probability/Fin_Map.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle