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 stray thm command
authorpaulson <lp15@cam.ac.uk>
Mon, 23 May 2016 16:03:29 +0100
changeset 63126 2b50f79829d2
parent 63125 f2d3f8427bc2
child 63127 360d9997fac9
deleted stray thm command
src/HOL/Multivariate_Analysis/Path_Connected.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon May 23 16:02:46 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon May 23 16:03:29 2016 +0100
@@ -5252,7 +5252,6 @@
 
 subsection\<open>Existence of isometry between subspaces of same dimension\<close>
 
-thm subspace_isomorphism
 lemma isometry_subset_subspace:
   fixes S :: "'a::euclidean_space set"
     and T :: "'b::euclidean_space set"
isabelle