equal
deleted
inserted
replaced
10 |
10 |
11 section \<open>Random Permutations\<close> |
11 section \<open>Random Permutations\<close> |
12 |
12 |
13 theory Random_Permutations |
13 theory Random_Permutations |
14 imports |
14 imports |
15 "~~/src/HOL/Probability/Probability_Mass_Function" |
15 Probability_Mass_Function |
16 "HOL-Library.Multiset_Permutations" |
16 "HOL-Library.Multiset_Permutations" |
17 begin |
17 begin |
18 |
18 |
19 text \<open> |
19 text \<open> |
20 Choosing a set permutation (i.e. a distinct list with the same elements as the set) |
20 Choosing a set permutation (i.e. a distinct list with the same elements as the set) |