src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
changeset 63075 60a42a4166af
parent 63016 3590590699b1
child 63332 f164526d8727
     1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon May 09 16:02:23 2016 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon May 09 17:23:19 2016 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  lemma delta_mult_idempotent:
     1.6    "(if k=a then 1 else (0::'a::semiring_1)) * (if k=a then 1 else 0) = (if k=a then 1 else 0)"
     1.7 -  by (cases "k=a") auto
     1.8 +  by simp
     1.9  
    1.10  lemma setsum_UNIV_sum:
    1.11    fixes g :: "'a::finite + 'b::finite \<Rightarrow> _"
    1.12 @@ -812,7 +812,6 @@
    1.13        have "x \<in> span (columns A)"
    1.14          unfolding y[symmetric]
    1.15          apply (rule span_setsum)
    1.16 -        apply clarify
    1.17          unfolding scalar_mult_eq_scaleR
    1.18          apply (rule span_mul)
    1.19          apply (rule span_superset)