changeset 65515 | f595b7532dc9 |
parent 65511 | ea42dfd95ec8 |
child 65544 | c09c11386ca5 |
--- a/NEWS Thu Apr 20 10:45:52 2017 +0200 +++ b/NEWS Thu Apr 20 16:21:28 2017 +0200 @@ -154,6 +154,8 @@ * Session HOL-Algebra extended by additional lattice theory: the Knaster-Tarski fixed point theorem and Galois Connections. +* SMT module: The legacy module 'src/HOL/Library/Old_SMT.thy' has been removed. + * 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.