src/HOL/Analysis/Connected.thy

   for s :: "'a::euclidean_space set"
   using complete_eq_closed closed_subspace by auto
 
 lemma closed_span [iff]: "closed (span s)"
   for s :: "'a::euclidean_space set"
-  by (simp add: closed_subspace)
+  by (simp add: closed_subspace subspace_span)
 
 lemma dim_closure [simp]: "dim (closure s) = dim s" (is "?dc = ?d")
   for s :: "'a::euclidean_space set"
 proof -
   have "?dc \<le> ?d"
-    using closure_minimal[OF span_inc, of s]
+    using closure_minimal[OF span_superset, of s]
     using closed_subspace[OF subspace_span, of s]
     using dim_subset[of "closure s" "span s"]
     by simp
   then show ?thesis
     using dim_subset[OF closure_subset, of s]