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.