# HG changeset patch
# User himmelma
# Date 1267524437 -3600
# Node ID 7b1179be2ac51bdcd08705cd7b97c6303b1a6bc2
# Parent  3d073a3e1c61e415dc0006588dd6e8632e74c3e3
tuned

diff -r 3d073a3e1c61 -r 7b1179be2ac5 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue Mar 02 09:57:49 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue Mar 02 11:07:17 2010 +0100
@@ -3611,8 +3611,8 @@
       {fix x assume xs: "x \<in> s"
         have t: "t \<subseteq> (insert b (insert a (t -{b})))" using b by auto
         from b(1) have "b \<in> span t" by (simp add: span_superset)
-        have bs: "b \<in> span (insert a (t - {b}))"
-          by (metis in_span_delete a sp mem_def subset_eq)
+        have bs: "b \<in> span (insert a (t - {b}))" apply(rule in_span_delete)
+          using  a sp unfolding subset_eq by auto
         from xs sp have "x \<in> span t" by blast
         with span_mono[OF t]
         have x: "x \<in> span (insert b (insert a (t - {b})))" ..
@@ -3970,7 +3970,8 @@
 qed
 
 lemma span_eq: "span S = span T \<longleftrightarrow> S \<subseteq> span T \<and> T \<subseteq> span S"
-  by (metis set_eq_subset span_mono span_span span_inc) (* FIXME: slow *)
+  using span_inc[unfolded subset_eq] using span_mono[of T "span S"] span_mono[of S "span T"]
+  by(auto simp add: span_span)
 
 (* ------------------------------------------------------------------------- *)
 (* Low-dimensional subset is in a hyperplane (weak orthogonal complement).   *)