--- a/NEWS Tue May 24 22:46:23 2016 +0200
+++ b/NEWS Wed May 25 12:24:00 2016 +0200
@@ -93,6 +93,14 @@
*** HOL ***
+* Probability/Random_Permutations.thy contains some theory about
+choosing a permutation of a set uniformly at random and folding over a
+list in random order.
+
+* Library/Set_Permutations.thy (executably) defines the set of
+permutations of a set, i.e. the set of all lists that contain every
+element of the carrier set exactly once.
+
* New abbreviations for negated existence (but not bounded existence):
\<nexists>x. P x \<equiv> \<not> (\<exists>x. P x)