src/HOL/Analysis/Further_Topology.thy

--- a/src/HOL/Analysis/Further_Topology.thy	Wed Oct 26 11:35:41 2016 +0200
+++ b/src/HOL/Analysis/Further_Topology.thy	Wed Oct 26 12:22:58 2016 +0100
@@ -2959,9 +2959,6 @@
     using not_less by blast
 qed
 
-
-subsection\<open> Dimension-based conditions for various homeomorphisms.\<close>
-
 lemma simply_connected_sphere:
   fixes a :: "'a::euclidean_space"
   assumes "3 \<le> DIM('a)"