Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Deleted spurious markup
authorpaulson <lp15@cam.ac.uk>
Wed, 26 Oct 2016 12:22:58 +0100
changeset 64403 7fa053298f67
parent 64402 4f0acbd97491
child 64404 d75397e0aad5
Deleted spurious markup
src/HOL/Analysis/Further_Topology.thy file | annotate | diff | comparison | revisions 
--- 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)"
isabelle