NEWS
changeset 65515 f595b7532dc9
parent 65511 ea42dfd95ec8
child 65544 c09c11386ca5
     1.1 --- a/NEWS	Thu Apr 20 10:45:52 2017 +0200
     1.2 +++ b/NEWS	Thu Apr 20 16:21:28 2017 +0200
     1.3 @@ -154,6 +154,8 @@
     1.4  * Session HOL-Algebra extended by additional lattice theory: the
     1.5  Knaster-Tarski fixed point theorem and Galois Connections.
     1.6  
     1.7 +* SMT module: The legacy module 'src/HOL/Library/Old_SMT.thy' has been removed.
     1.8 +
     1.9  * Session HOL-Analysis: more material involving arcs, paths, covering
    1.10  spaces, innessential maps, retracts. Major results include the Jordan
    1.11  Curve Theorem and the Great Picard Theorem.