# HG changeset patch # User hoelzl # Date 1319803819 -7200 # Node ID fc3c7db5bb2f07dfe573951515aa7bf569308ad6 # Parent 97df8c08291c3c4f06b88aea2ca10d97cec889b9 correct import path diff -r 97df8c08291c -r fc3c7db5bb2f src/HOL/Probability/Borel_Space.thy --- a/src/HOL/Probability/Borel_Space.thy Fri Oct 28 14:06:06 2011 +0200 +++ b/src/HOL/Probability/Borel_Space.thy Fri Oct 28 14:10:19 2011 +0200 @@ -6,7 +6,7 @@ header {*Borel spaces*} theory Borel_Space - imports Sigma_Algebra "~~/src/HOL/Multvariate_Analysis/Multivariate_Analysis" + imports Sigma_Algebra "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis" begin section "Generic Borel spaces"