src/HOL/Probability/Random_Permutations.thy
changeset 73975 8d93f9ca6518
parent 73477 1d8a79aa2a99