--- a/NEWS Wed May 25 11:50:58 2016 +0200
+++ b/NEWS Wed May 25 13:13:35 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)