--- a/NEWS Fri Mar 03 23:21:24 2017 +0100
+++ b/NEWS Thu Mar 02 21:16:02 2017 +0100
@@ -108,6 +108,9 @@
with type class annotations. As a result, the tactic that derives
it no longer fails on nested datatypes. Slight INCOMPATIBILITY.
+* Session HOL-Algebra extended by additional lattice theory: the
+Knaster-Tarski fixed point theorem and Galois Connections.
+
* Session HOL-Analysis: more material involving arcs, paths, covering
spaces, innessential maps, retracts. Major results include the Jordan
Curve Theorem and the Great Picard Theorem.