--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Mon May 09 16:02:23 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Mon May 09 17:23:19 2016 +0100
@@ -9,7 +9,7 @@
lemma delta_mult_idempotent:
"(if k=a then 1 else (0::'a::semiring_1)) * (if k=a then 1 else 0) = (if k=a then 1 else 0)"
- by (cases "k=a") auto
+ by simp
lemma setsum_UNIV_sum:
fixes g :: "'a::finite + 'b::finite \<Rightarrow> _"
@@ -812,7 +812,6 @@
have "x \<in> span (columns A)"
unfolding y[symmetric]
apply (rule span_setsum)
- apply clarify
unfolding scalar_mult_eq_scaleR
apply (rule span_mul)
apply (rule span_superset)