Set_Permutations -> Multiset_Permutations in NEWS
authoreberlm <eberlm@in.tum.de>
Fri Oct 07 10:45:21 2016 +0200 (2016-10-07)
changeset 640747dccbbd8d71d
parent 64073 cffd5f537206
child 64075 3d4c3eec5143
Set_Permutations -> Multiset_Permutations in NEWS
NEWS
     1.1 --- a/NEWS	Fri Oct 07 10:31:34 2016 +0200
     1.2 +++ b/NEWS	Fri Oct 07 10:45:21 2016 +0200
     1.3 @@ -429,9 +429,9 @@
     1.4  "unbundle finfun_syntax" to imitate import of
     1.5  "~~/src/HOL/Library/FinFun_Syntax".
     1.6  
     1.7 -* HOL-Library: theory Set_Permutations (executably) defines the set of
     1.8 -permutations of a set, i.e. the set of all lists that contain every
     1.9 -element of the carrier set exactly once.
    1.10 +* HOL-Library: theory Multiset_Permutations (executably) defines the set of
    1.11 +permutations of a given set or multiset, i.e. the set of all lists that 
    1.12 +contain every element of the carrier (multi-)set exactly once.
    1.13  
    1.14  * HOL-Library: multiset membership is now expressed using set_mset
    1.15  rather than count.