# HG changeset patch
# User eberlm
# Date 1464097450 -7200
# Node ID 6a17bcddd6c2b71654851c696bd248d1cceb3b20
# Parent  b29a8f57e3a0d1c91fe59e55b57a625646a40de4
Resolved cyclic dependency of theories

diff -r b29a8f57e3a0 -r 6a17bcddd6c2 src/HOL/Probability/Random_Permutations.thy
--- a/src/HOL/Probability/Random_Permutations.thy	Tue May 24 15:05:59 2016 +0200
+++ b/src/HOL/Probability/Random_Permutations.thy	Tue May 24 15:44:10 2016 +0200
@@ -11,7 +11,7 @@
 section \<open>Random Permutations\<close>
 
 theory Random_Permutations
-imports "~~/src/HOL/Probability/Probability" "~~/src/HOL/Library/Set_Permutations"
+imports "~~/src/HOL/Probability/Probability_Mass_Function" "~~/src/HOL/Library/Set_Permutations"
 begin
 
 text \<open>