NEWS
changeset 65099 30d0b2f1df76
parent 65073 b5bf76cf2b4e
child 65170 53675f36820d
     1.1 --- a/NEWS	Fri Mar 03 23:21:24 2017 +0100
     1.2 +++ b/NEWS	Thu Mar 02 21:16:02 2017 +0100
     1.3 @@ -108,6 +108,9 @@
     1.4      with type class annotations. As a result, the tactic that derives
     1.5      it no longer fails on nested datatypes. Slight INCOMPATIBILITY.
     1.6  
     1.7 +* Session HOL-Algebra extended by additional lattice theory: the
     1.8 +Knaster-Tarski fixed point theorem and Galois Connections.
     1.9 +
    1.10  * Session HOL-Analysis: more material involving arcs, paths, covering
    1.11  spaces, innessential maps, retracts. Major results include the Jordan
    1.12  Curve Theorem and the Great Picard Theorem.