diff -r bdcc11b2fdc8 -r 510ac30f44c0 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Fri Aug 12 07:18:28 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Fri Aug 12 09:17:24 2011 -0700
@@ -762,7 +762,7 @@
 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")
@@ -785,12 +785,12 @@
 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
@@ -830,7 +830,7 @@
     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