# HG changeset patch
# User huffman
# Date 1379001832 25200
# Node ID a7bcbb5a17d8455ccea445d291cf5a88c50b551d
# Parent  b6dc5403cad1188effc89c327c15b23c32151836
removed outdated comments

diff -r b6dc5403cad1 -r a7bcbb5a17d8 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Fri Sep 13 00:55:44 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Sep 12 09:03:52 2013 -0700
@@ -322,7 +322,6 @@
   shows "setsum (\<lambda>x. c *s f x) S = c *s setsum f S"
   by (simp add: vec_eq_iff setsum_right_distrib)
 
-(* TODO: use setsum_norm_allsubsets_bound *)
 lemma setsum_norm_allsubsets_bound_cart:
   fixes f:: "'a \<Rightarrow> real ^'n"
   assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (setsum f Q) \<le> e"
diff -r b6dc5403cad1 -r a7bcbb5a17d8 src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Fri Sep 13 00:55:44 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Thu Sep 12 09:03:52 2013 -0700
@@ -587,7 +587,7 @@
 qed
 
 lemma open_path_component:
-  fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*)
+  fixes s :: "'a::real_normed_vector set"
   assumes "open s"
   shows "open {y. path_component s x y}"
   unfolding open_contains_ball
@@ -620,7 +620,7 @@
 qed
 
 lemma open_non_path_component:
-  fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*)
+  fixes s :: "'a::real_normed_vector set"
   assumes "open s"
   shows "open(s - {y. path_component s x y})"
   unfolding open_contains_ball
@@ -648,7 +648,7 @@
 qed
 
 lemma connected_open_path_connected:
-  fixes s :: "'a::real_normed_vector set" (*TODO: generalize to metric_space*)
+  fixes s :: "'a::real_normed_vector set"
   assumes "open s" "connected s"
   shows "path_connected s"
   unfolding path_connected_component_set