# HG changeset patch
# User eberlm
# Date 1464171840 -7200
# Node ID 76130b7cc450b5985f95972bfa897f40b2164dfc
# Parent  ef72b104fa323eb8980b039e776040c372917885
NEWS: Permutations of a set and randomised folds

diff -r ef72b104fa32 -r 76130b7cc450 NEWS
--- 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)