src/HOL/Matrix/Matrix.thy
changeset 29700 22faf21db3df
parent 29667 53103fc8ffa3
child 32440 153965be0f4b
     1.1 --- a/src/HOL/Matrix/Matrix.thy	Fri Jan 30 13:41:45 2009 +0000
     1.2 +++ b/src/HOL/Matrix/Matrix.thy	Sat Jan 31 09:04:16 2009 +0100
     1.3 @@ -1005,15 +1005,8 @@
     1.4    apply (subst foldseq_almostzero[of _ j])
     1.5    apply (simp add: prems)+
     1.6    apply (auto)
     1.7 -  proof -
     1.8 -    fix k
     1.9 -    fix l
    1.10 -    assume a:"~neg(int l - int i)"
    1.11 -    assume b:"nat (int l - int i) = 0"
    1.12 -    from a b have a: "l = i" by(insert not_neg_nat[of "int l - int i"], simp add: a b)
    1.13 -    assume c: "i \<noteq> l"
    1.14 -    from c a show "fmul (Rep_matrix A k j) e = 0" by blast
    1.15 -  qed
    1.16 +  apply (metis comm_monoid_add.mult_1 le_anti_sym le_diff_eq not_neg_nat zero_le_imp_of_nat zle_int)
    1.17 +  done
    1.18  
    1.19  lemma mult_matrix_ext:
    1.20    assumes