diff -r 49c312eaaa11 -r 81b7832b29a3 src/HOL/Matrix/SparseMatrix.thy
--- a/src/HOL/Matrix/SparseMatrix.thy	Wed Aug 02 16:50:41 2006 +0200
+++ b/src/HOL/Matrix/SparseMatrix.thy	Wed Aug 02 18:19:48 2006 +0200
@@ -338,17 +338,12 @@
     apply (subst Rep_matrix_mult)
     apply (rule_tac j1=aa in ssubst[OF foldseq_almostzero])
     apply (simp_all)
-    apply (intro strip, rule conjI)
     apply (intro strip)
-    apply (drule_tac max_helper)
-    apply (simp)
-    apply (auto)
     apply (rule zero_imp_mult_zero)
     apply (rule disjI2)
     apply (rule nrows)
     apply (rule order_trans[of _ 1])
-    apply (simp)
-    apply (simp)
+    apply auto
     done
 qed