author | eberlm <eberlm@in.tum.de> |

Fri Oct 07 10:45:21 2016 +0200 (2016-10-07) | |

changeset 64074 | 7dccbbd8d71d |

parent 64073 | cffd5f537206 |

child 64075 | 3d4c3eec5143 |

Set_Permutations -> Multiset_Permutations in 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.