author | eberlm |
Tue, 24 May 2016 15:44:10 +0200 | |
changeset 63124 | 6a17bcddd6c2 |
parent 63123 | b29a8f57e3a0 |
child 63131 | 76cb6c6bd7b8 |
--- 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>