Resolved cyclic dependency of theories
authoreberlm
Tue, 24 May 2016 15:44:10 +0200
changeset 63124 6a17bcddd6c2
parent 63123 b29a8f57e3a0
child 63131 76cb6c6bd7b8
Resolved cyclic dependency of theories
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>