src/HOL/Probability/Random_Permutations.thy
changeset 73527 c72fd8f1fceb
parent 73477 1d8a79aa2a99
equal deleted inserted replaced
73525:419edc7f3726 73527:c72fd8f1fceb