--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Mon Sep 12 07:55:43 2011 +0200
@@ -1256,7 +1256,7 @@
have "x\<in>UNIV" by auto from this[unfolded span_basis[THEN sym]]
have "\<exists>u. (\<Sum>v\<in>basis ` {..<DIM('a)}. u v *\<^sub>R v) = x"
unfolding range_basis span_insert_0 apply(subst (asm) span_finite) by auto
- thus ?thesis by fastsimp
+ thus ?thesis by fastforce
qed
lemma span_basis'[simp]:"span ((basis::nat=>'a) ` {..<DIM('a::euclidean_space)}) = UNIV"