src/HOL/Analysis/Starlike.thy

     proof (rule span_sum[of D "(\<lambda>b. b /\<^sub>R (2 * real (card D)))" D])
       {
         fix x :: "'a::euclidean_space"
         assume "x \<in> D"
         then have "x \<in> span D"
-          using span_superset[of _ "D"] by auto
+          using span_base[of _ "D"] by auto
         then have "x /\<^sub>R (2 * real (card D)) \<in> span D"
           using span_mul[of x "D" "(inverse (real (card D)) / 2)"] by auto
       }
       then show "\<And>x. x\<in>D \<Longrightarrow> x /\<^sub>R (2 * real (card D)) \<in> span D"
         by auto

 
 lemma dim_special_hyperplane:
   fixes k :: "'n::euclidean_space"
   shows "k \<in> Basis \<Longrightarrow> dim {x. k \<bullet> x = 0} = DIM('n) - 1"
 apply (simp add: special_hyperplane_span)
-apply (rule Linear_Algebra.dim_unique [OF subset_refl])
+apply (rule dim_unique [OF subset_refl])
 apply (auto simp: Diff_subset independent_substdbasis)
-apply (metis member_remove remove_def span_superset)
+apply (metis member_remove remove_def span_base)
 done
 
 proposition dim_hyperplane:
   fixes a :: "'a::euclidean_space"
   assumes "a \<noteq> 0"

     done
   have "span (S \<union> insert a' U) = span (insert a' (S \<union> T))"
     using spanU by simp
   also have "... = span (insert a (S \<union> T))"
     apply (rule eq_span_insert_eq)
-    apply (simp add: a'_def span_neg span_sum span_superset span_mul)
+    apply (simp add: a'_def span_neg span_sum span_base span_mul)
     done
   also have "... = span (S \<union> insert a T)"
     by simp
   finally show ?case
     by (rule_tac x="insert a' U" in exI) (use orthU in auto)

   obtains y where "y \<noteq> 0" "orthogonal x y"
 proof -
   have "dim {x} < DIM('a)"
     using assms by auto
   then show thesis
-    by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_superset that)
+    by (rule orthogonal_to_subspace_exists) (simp add: orthogonal_commute span_base that)
 qed
 
 proposition%important orthogonal_subspace_decomp_exists:
   fixes S :: "'a :: euclidean_space set"
   obtains y z where "y \<in> span S" "\<And>w. w \<in> span S \<Longrightarrow> orthogonal z w" "x = y + z"

             moreover have "?y \<notin> U"
             proof -
               have "e/2 / norm a \<noteq> 0"
                 using \<open>0 < e\<close> \<open>a \<noteq> 0\<close> by auto
               then show ?thesis
-                by (metis True \<open>a \<noteq> 0\<close> a orthogonal_scaleR orthogonal_self real_vector.scale_eq_0_iff span_add_eq span_superset)
+                by (metis True \<open>a \<noteq> 0\<close> a orthogonal_scaleR orthogonal_self real_vector.scale_eq_0_iff span_add_eq span_base)
             qed
             ultimately show "?y \<in> S - U" by blast
           qed
         next
           case False

   { fix v
     let ?u = "\<Sum>b\<in>B. (v \<bullet> b) *\<^sub>R b"
     have "v = ?u + (v - ?u)"
       by simp
     moreover have "?u \<in> U"
-      by (metis (no_types, lifting) \<open>span B = U\<close> assms real_vector_class.subspace_sum span_superset span_mul)
+      by (metis (no_types, lifting) \<open>span B = U\<close> assms subspace_sum span_base span_mul)
     moreover have "(v - ?u) \<in> U\<^sup>\<bottom>"
     proof (clarsimp simp: orthogonal_comp_def orthogonal_def)
       fix y
       assume "y \<in> U"
       with \<open>span B = U\<close> span_finite [OF \<open>finite B\<close>]