diff -r 10644973cdde -r 42cc3609fedf src/HOL/Analysis/Elementary_Topology.thy
--- 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