# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1464015809 -3600
# Node ID 2b50f79829d24bfbecc1dcbc9aaebb9ab8fa467d
# Parent  f2d3f8427bc27412fd4a839dd62ef6ec4ba9fe97
deleted stray thm command

diff -r f2d3f8427bc2 -r 2b50f79829d2 src/HOL/Multivariate_Analysis/Path_Connected.thy
--- 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"