NEWS
changeset 66643 f7e38b8583a0
parent 66641 ff2e0115fea4
child 66650 bcea02893d17
     1.1 --- a/NEWS	Fri Sep 08 12:49:40 2017 +0100
     1.2 +++ b/NEWS	Fri Sep 08 15:27:22 2017 +0100
     1.3 @@ -220,7 +220,7 @@
     1.4  * Theory "HOL-Library.Permutations": theorem bij_swap_ompose_bij has
     1.5  been renamed to bij_swap_compose_bij. INCOMPATIBILITY.
     1.6  
     1.7 -* New theory "HOL-Library.Going_To_Filter" providing the "f going_to F" 
     1.8 +* New theory "HOL-Library.Going_To_Filter" providing the "f going_to F"
     1.9  filter for describing points x such that f(x) is in the filter F.
    1.10  
    1.11  * Theory "HOL-Library.Formal_Power_Series": constants X/E/L/F have been
    1.12 @@ -255,7 +255,7 @@
    1.13  
    1.14  * Session HOL-Analysis: more material involving arcs, paths, covering
    1.15  spaces, innessential maps, retracts, infinite products, simplicial complexes.
    1.16 -Baire Category theory. Major results include the Jordan Curve Theorem and the Great Picard
    1.17 +Baire Category theorem. Major results include the Jordan Curve Theorem and the Great Picard
    1.18  Theorem.
    1.19  
    1.20  * Session HOL-Algebra has been extended by additional lattice theory: