--- a/src/HOL/Analysis/Elementary_Topology.thy Sun Jan 06 16:27:52 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Topology.thy Sun Jan 06 17:54:49 2019 +0100
@@ -2096,4 +2096,5 @@
using T_def by (auto elim!: eventually_mono)
qed
+
end
\ No newline at end of file