NEWS
changeset 70168 e79bbf86a984
parent 70164 1f163f772da3
child 70174 40fdd74b75f3
     1.1 --- a/NEWS	Tue Apr 16 19:42:56 2019 +0200
     1.2 +++ b/NEWS	Tue Apr 16 20:00:14 2019 +0200
     1.3 @@ -249,8 +249,8 @@
     1.4  precedence as any other prefix function symbol.
     1.5  
     1.6  * Theory HOL-Library.Cardinal_Notations has been discontinued in favor
     1.7 -of the bundle cardinal_syntax (available in Main).
     1.8 -Minor INCOMPATIBILITY.
     1.9 +of the bundle cardinal_syntax (available in theory Main). Minor
    1.10 +INCOMPATIBILITY.
    1.11  
    1.12  * Session HOL-Library and HOL-Number_Theory: Exponentiation by squaring,
    1.13  used for computing powers in class "monoid_mult" and modular
    1.14 @@ -262,15 +262,16 @@
    1.15  * Session HOL-Number_Theory: More material on residue rings in
    1.16  Carmichael's function, primitive roots, more properties for "ord".
    1.17  
    1.18 -* Session HOL-Homology: New, a port of HOL Light's homology library,
    1.19 -with new proofs of "invariance of domain" and related results.
    1.20 -
    1.21  * Session HOL-Analysis: Better organization and much more material
    1.22  at the level of abstract topological spaces.
    1.23  
    1.24  * Session HOL-Algebra: Free abelian groups, etc., ported from HOL Light;
    1.25  proofs towards algebraic closure by de Vilhena and Baillon.
    1.26  
    1.27 +* Session HOL-Homology has been added. It is a port of HOL Light's
    1.28 +homology library, with new proofs of "invariance of domain" and related
    1.29 +results.
    1.30 +
    1.31  * Session HOL-SPARK: .prv files are no longer written to the
    1.32  file-system, but exported to the session database. Results may be
    1.33  retrieved via "isabelle build -e HOL-SPARK-Examples" on the