# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1464015766 -3600
# Node ID f2d3f8427bc27412fd4a839dd62ef6ec4ba9fe97
# Parent  39dca48916014791aa63cab1f2872a67d0194dcb
deleted needless comment

diff -r 39dca4891601 -r f2d3f8427bc2 src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon May 23 15:46:30 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Mon May 23 16:02:46 2016 +0100
@@ -5412,7 +5412,6 @@
     done
 qed
 
-(*REPLACE*)
 lemma isometry_subspaces:
   fixes S :: "'a::euclidean_space set"
     and T :: "'b::euclidean_space set"