tuned proofs
authornipkow
Fri Aug 28 19:49:05 2009 +0200 (2009-08-28 ago)
changeset 32440153965be0f4b
parent 32439 7a91c7bcfe7e
child 32441 0273a2f787ea
tuned proofs
src/HOL/Matrix/Matrix.thy
     1.1 --- a/src/HOL/Matrix/Matrix.thy	Fri Aug 28 19:43:19 2009 +0200
     1.2 +++ b/src/HOL/Matrix/Matrix.thy	Fri Aug 28 19:49:05 2009 +0200
     1.3 @@ -1663,7 +1663,7 @@
     1.4  apply (simp add: times_matrix_def Rep_mult_matrix)
     1.5  apply (rule_tac j1="xa" in ssubst[OF foldseq_almostzero])
     1.6  apply (simp_all)
     1.7 -by (simp add: max_def ncols)
     1.8 +by (simp add: ncols)
     1.9  
    1.10  lemma one_matrix_mult_left[simp]: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = (A::('a::ring_1) matrix)"
    1.11  apply (subst Rep_matrix_inject[THEN sym])
    1.12 @@ -1671,7 +1671,7 @@
    1.13  apply (simp add: times_matrix_def Rep_mult_matrix)
    1.14  apply (rule_tac j1="x" in ssubst[OF foldseq_almostzero])
    1.15  apply (simp_all)
    1.16 -by (simp add: max_def nrows)
    1.17 +by (simp add: nrows)
    1.18  
    1.19  lemma transpose_matrix_mult: "transpose_matrix ((A::('a::comm_ring) matrix)*B) = (transpose_matrix B) * (transpose_matrix A)"
    1.20  apply (simp add: times_matrix_def)