src/HOL/Probability/Random_Permutations.thy

 
 
 text \<open>
   A generic fold function that takes a function, an initial state, and a set 
   and chooses a random order in which it then traverses the set in the same 
-  fashion as a left-fold over a list.
+  fashion as a left fold over a list.
     We first give a recursive definition.
 \<close>
 function fold_random_permutation :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b pmf" where
   "fold_random_permutation f x {} = return_pmf x"
 | "\<not>finite A \<Longrightarrow> fold_random_permutation f x A = return_pmf x"