--- a/NEWS Thu Aug 17 21:12:55 2017 +0200
+++ b/NEWS Thu Aug 17 22:29:30 2017 +0200
@@ -121,6 +121,10 @@
*** HOL ***
+* Constant "subseq" in Topological_Spaces removed and subsumed by
+"strict_mono". Some basic lemmas specific to "subseq" have been renamed
+accordingly, e.g. "subseq_o" -> "strict_mono_o" etc.
+
* Command and antiquotation "value" with modified default strategy:
terms without free variables are always evaluated using plain evaluation
only, with no fallback on normalization by evaluation.