src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy

 apply (rule span_setsum)
 apply simp
 apply auto
 apply (rule span_mul)
 apply (rule span_superset)
-apply (auto simp add: Collect_def mem_def)
+apply auto
 done
 
 lemma finite_stdbasis: "finite {cart_basis i ::real^'n |i. i\<in> (UNIV:: 'n set)}" (is "finite ?S")
 proof-
   have eq: "?S = cart_basis ` UNIV" by blast

   and iS: "i \<notin> S"
   shows "(x$i) = 0"
 proof-
   let ?U = "UNIV :: 'n set"
   let ?B = "cart_basis ` S"
-  let ?P = "\<lambda>(x::real^_). \<forall>i\<in> ?U. i \<notin> S \<longrightarrow> x$i =0"
+  let ?P = "{(x::real^_). \<forall>i\<in> ?U. i \<notin> S \<longrightarrow> x$i =0}"
  {fix x::"real^_" assume xS: "x\<in> ?B"
-   from xS have "?P x" by auto}
+   from xS have "x \<in> ?P" by auto}
  moreover
  have "subspace ?P"
-   by (auto simp add: subspace_def Collect_def mem_def)
+   by (auto simp add: subspace_def)
  ultimately show ?thesis
    using x span_induct[of ?B ?P x] iS by blast
 qed
 
 lemma independent_stdbasis: "independent {cart_basis i ::real^'n |i. i\<in> (UNIV :: 'n set)}"

   let ?I = "{cart_basis i:: real^'m|i. i \<in> ?U}"
   {fix x assume x: "x \<in> (UNIV :: (real^'m) set)"
     from equalityD2[OF span_stdbasis]
     have IU: " (UNIV :: (real^'m) set) \<subseteq> span ?I" by blast
     from linear_eq[OF lf lg IU] fg x
-    have "f x = g x" unfolding Collect_def  Ball_def mem_def by metis}
+    have "f x = g x" unfolding Ball_def mem_Collect_eq by metis}
   then show ?thesis by (auto intro: ext)
 qed
 
 lemma bilinear_eq_stdbasis_cart:
   assumes bf: "bilinear (f:: real^'m \<Rightarrow> real^'n \<Rightarrow> _)"