--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Tue May 24 18:46:51 2016 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Tue May 24 18:48:01 2016 +0200
@@ -73,6 +73,9 @@
lemma [code, code del]:
"Lcm_eucl = Lcm_eucl" ..
+lemma [code, code del]:
+ "permutations_of_set = permutations_of_set" ..
+
(*
If the code generation ends with an exception with the following message:
'"List.set" is not a constructor, on left hand side of equation: ...',
--- a/src/HOL/Probability/Random_Permutations.thy Tue May 24 18:46:51 2016 +0200
+++ b/src/HOL/Probability/Random_Permutations.thy Tue May 24 18:48:01 2016 +0200
@@ -40,7 +40,7 @@
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