changeset 66453 | cc19f7ca2ed6 |
parent 65395 | 7504569a73c7 |
child 67399 | eab6ce8368fa |
--- a/src/HOL/Probability/Random_Permutations.thy Fri Aug 18 13:55:05 2017 +0200 +++ b/src/HOL/Probability/Random_Permutations.thy Fri Aug 18 20:47:47 2017 +0200 @@ -13,7 +13,7 @@ theory Random_Permutations imports "~~/src/HOL/Probability/Probability_Mass_Function" - "~~/src/HOL/Library/Multiset_Permutations" + "HOL-Library.Multiset_Permutations" begin text \<open>