changeset 72671 | 588c751a5eef |
parent 71989 | bad75618fb82 |
child 73477 | 1d8a79aa2a99 |
--- a/src/HOL/Probability/Random_Permutations.thy Fri Nov 20 23:53:37 2020 +0100 +++ b/src/HOL/Probability/Random_Permutations.thy Sat Nov 21 00:29:41 2020 +0100 @@ -12,7 +12,7 @@ theory Random_Permutations imports - "~~/src/HOL/Probability/Probability_Mass_Function" + Probability_Mass_Function "HOL-Library.Multiset_Permutations" begin