summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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

Fri, 07 Oct 2016 10:45:21 +0200 | |

changeset 64074 | 7dccbbd8d71d |

parent 64073 | cffd5f537206 |

child 64075 | 3d4c3eec5143 |

Set_Permutations -> Multiset_Permutations in NEWS

--- a/NEWS Fri Oct 07 10:31:34 2016 +0200 +++ b/NEWS Fri Oct 07 10:45:21 2016 +0200 @@ -429,9 +429,9 @@ "unbundle finfun_syntax" to imitate import of "~~/src/HOL/Library/FinFun_Syntax". -* HOL-Library: theory Set_Permutations (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. +* HOL-Library: theory Multiset_Permutations (executably) defines the set of +permutations of a given set or multiset, i.e. the set of all lists that +contain every element of the carrier (multi-)set exactly once. * HOL-Library: multiset membership is now expressed using set_mset rather than count.