--- a/src/HOL/Multivariate_Analysis/Determinants.thy Mon May 09 16:02:23 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy Mon May 09 17:23:19 2016 +0100
@@ -836,7 +836,6 @@
unfolding thr0
apply (rule span_setsum)
apply simp
- apply (rule ballI)
apply (rule span_mul [where 'a="real^'n", folded scalar_mult_eq_scaleR])+
apply (rule span_superset)
apply auto
@@ -878,7 +877,6 @@
have thd0: "det (\<chi> i. if i = k then row k A + (\<Sum>i \<in> ?Uk. x $ i *s row i A) else row i A) = det A"
apply (rule det_row_span)
apply (rule span_setsum)
- apply (rule ballI)
apply (rule span_mul [where 'a="real^'n", folded scalar_mult_eq_scaleR])+
apply (rule span_superset)
apply auto