summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

NEWS

changeset 64122 | 74fde524799e |

parent 64113 | 86efd3d4dc98 |

child 64240 | eabf80376aab |

1.1 --- a/NEWS Sun Oct 09 16:27:01 2016 +0200 1.2 +++ b/NEWS Mon Oct 10 15:45:41 2016 +0100 1.3 @@ -432,7 +432,7 @@ 1.4 "~~/src/HOL/Library/FinFun_Syntax". 1.5 1.6 * HOL-Library: theory Multiset_Permutations (executably) defines the set of 1.7 -permutations of a given set or multiset, i.e. the set of all lists that 1.8 +permutations of a given set or multiset, i.e. the set of all lists that 1.9 contain every element of the carrier (multi-)set exactly once. 1.10 1.11 * HOL-Library: multiset membership is now expressed using set_mset 1.12 @@ -485,8 +485,7 @@ 1.13 and the Kreinâ€“Milman Minkowski theorem. 1.14 1.15 * HOL-Analysis: Numerous results ported from the HOL Light libraries: 1.16 -homeomorphisms, continuous function extensions and other advanced topics 1.17 -in topology 1.18 +homeomorphisms, continuous function extensions, invariance of domain. 1.19 1.20 * HOL-Probability: the type of emeasure and nn_integral was changed from 1.21 ereal to ennreal, INCOMPATIBILITY.