diff -r f13a762f7d96 -r 1557a391a858 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Feb 27 15:19:09 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Feb 27 16:07:21 2014 +0000
@@ -925,17 +925,10 @@
   by (rule subspace_setsum, rule subspace_span)
 
 lemma span_add_eq: "x \<in> span S \<Longrightarrow> x + y \<in> span S \<longleftrightarrow> y \<in> span S"
-  apply (auto simp only: span_add span_sub)
-  apply (subgoal_tac "(x + y) - x \<in> span S")
-  apply simp
-  apply (simp only: span_add span_sub)
-  done
+  by (metis add_minus_cancel scaleR_minus1_left subspace_def subspace_span)
 
 text {* Mapping under linear image. *}
 
-lemma image_subset_iff_subset_vimage: "f ` A \<subseteq> B \<longleftrightarrow> A \<subseteq> f -` B"
-  by auto (* TODO: move *)
-
 lemma span_linear_image:
   assumes lf: "linear f"
   shows "span (f ` S) = f ` (span S)"
@@ -1271,29 +1264,13 @@
     assume i: ?rhs
     show ?lhs
       using i False
-      apply simp
       apply (auto simp add: dependent_def)
-      apply (case_tac "aa = a")
-      apply auto
-      apply (subgoal_tac "insert a S - {aa} = insert a (S - {aa})")
-      apply simp
-      apply (subgoal_tac "a \<in> span (insert aa (S - {aa}))")
-      apply (subgoal_tac "insert aa (S - {aa}) = S")
-      apply simp
-      apply blast
-      apply (rule in_span_insert)
-      apply assumption
-      apply blast
-      apply blast
-      done
+      by (metis in_span_insert insert_Diff insert_Diff_if insert_iff)
   qed
 qed
 
 text {* The degenerate case of the Exchange Lemma. *}
 
-lemma mem_delete: "x \<in> (A - {a}) \<longleftrightarrow> x \<noteq> a \<and> x \<in> A"
-  by blast
-
 lemma spanning_subset_independent:
   assumes BA: "B \<subseteq> A"
     and iA: "independent A"
@@ -1345,23 +1322,16 @@
   let ?P = "\<lambda>t'. card t' = card t \<and> finite t' \<and> s \<subseteq> t' \<and> t' \<subseteq> s \<union> t \<and> s \<subseteq> span t'"
   let ?ths = "\<exists>t'. ?P t'"
   {
-    assume st: "s \<subseteq> t"
-    from st ft span_mono[OF st]
-    have ?ths
-      apply -
-      apply (rule exI[where x=t])
-      apply (auto intro: span_superset)
-      done
+    assume "s \<subseteq> t"
+    then have ?ths
+      by (metis ft Un_commute sp sup_ge1)
   }
   moreover
   {
     assume st: "t \<subseteq> s"
     from spanning_subset_independent[OF st s sp] st ft span_mono[OF st]
     have ?ths
-      apply -
-      apply (rule exI[where x=t])
-      apply (auto intro: span_superset)
-      done
+      by (metis Un_absorb sp)
   }
   moreover
   {
@@ -3099,12 +3069,7 @@
   unfolding scaleR_scaleR
   unfolding norm_scaleR
   apply (subgoal_tac "norm x * c = \<bar>c\<bar> * norm x \<or> norm x * c = - \<bar>c\<bar> * norm x")
-  apply (case_tac "c \<le> 0", simp add: field_simps)
-  apply (simp add: field_simps)
-  apply (case_tac "c \<le> 0", simp add: field_simps)
-  apply (simp add: field_simps)
-  apply simp
-  apply simp
+  apply (auto simp add: field_simps)
   done
 
 end