# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1477480978 -3600
# Node ID 7fa053298f67b8c1b948998eb772ca59c5f494b3
# Parent  4f0acbd9749174f5f34ff9131c1da4f9c15412b3
Deleted spurious markup

diff -r 4f0acbd97491 -r 7fa053298f67 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)"