NEWS
changeset 70125 b601c2c87076
parent 70106 55220f2d09d2
child 70127 538d9854ca2f
     1.1 --- a/NEWS	Wed Apr 10 23:12:27 2019 +0100
     1.2 +++ b/NEWS	Thu Apr 11 15:26:04 2019 +0100
     1.3 @@ -243,10 +243,14 @@
     1.4  * Session HOL-Number_Theory: More material on residue rings in
     1.5  Carmichael's function, primitive roots, more properties for "ord".
     1.6  
     1.7 -* Session HOL-Analysis: Better organization and much more material,
     1.8 -including algebraic topology.
     1.9 -
    1.10 -* Session HOL-Algebra: Much more material on group theory.
    1.11 +* Session HOL-Homology: New, a port of HOL Light's homology library,
    1.12 +with new proofs of "invariance of domain" and related results.
    1.13 +
    1.14 +* Session HOL-Analysis: Better organization and much more material
    1.15 +at the level of abstract topological spaces.
    1.16 +
    1.17 +* Session HOL-Algebra: Much more material on group theory, mostly ported
    1.18 +from HOL Light.
    1.19  
    1.20  * Session HOL-SPARK: .prv files are no longer written to the
    1.21  file-system, but exported to the session database. Results may be