# HG changeset patch
# User nipkow
# Date 1251481745 -7200
# Node ID 153965be0f4b94e3a53b0d2c67c568aaab28cef7
# Parent  7a91c7bcfe7e7425e1ff8d18982911c1cd1a343b
tuned proofs

diff -r 7a91c7bcfe7e -r 153965be0f4b src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Fri Aug 28 19:43:19 2009 +0200
+++ b/src/HOL/Matrix/Matrix.thy	Fri Aug 28 19:49:05 2009 +0200
@@ -1663,7 +1663,7 @@
 apply (simp add: times_matrix_def Rep_mult_matrix)
 apply (rule_tac j1="xa" in ssubst[OF foldseq_almostzero])
 apply (simp_all)
-by (simp add: max_def ncols)
+by (simp add: ncols)
 
 lemma one_matrix_mult_left[simp]: "nrows A <= n \<Longrightarrow> (one_matrix n) * A = (A::('a::ring_1) matrix)"
 apply (subst Rep_matrix_inject[THEN sym])
@@ -1671,7 +1671,7 @@
 apply (simp add: times_matrix_def Rep_mult_matrix)
 apply (rule_tac j1="x" in ssubst[OF foldseq_almostzero])
 apply (simp_all)
-by (simp add: max_def nrows)
+by (simp add: nrows)
 
 lemma transpose_matrix_mult: "transpose_matrix ((A::('a::comm_ring) matrix)*B) = (transpose_matrix B) * (transpose_matrix A)"
 apply (simp add: times_matrix_def)