# HG changeset patch
# User eberlm <eberlm@in.tum.de>
# Date 1503001770 -7200
# Node ID a8299195ed82cc8a0eb22ff0185106edbfe0676b
# Parent  1be102db1598d6ea3ff7c9fd15f2a7d4d64c8397
NEWS: Removed constant subseq; subsumed by strict_mono

diff -r 1be102db1598 -r a8299195ed82 NEWS
--- 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.