# HG changeset patch
# User webertj
# Date 1154535588 -7200
# Node ID 81b7832b29a310d3f758f883a0950749e9ddd3c8
# Parent  49c312eaaa1103d0f538b595e33f4693a9ba38e7
lin_arith_prover splits certain operators (e.g. min, max, abs)

diff -r 49c312eaaa11 -r 81b7832b29a3 src/HOL/Matrix/MatrixGeneral.thy
--- a/src/HOL/Matrix/MatrixGeneral.thy	Wed Aug 02 16:50:41 2006 +0200
+++ b/src/HOL/Matrix/MatrixGeneral.thy	Wed Aug 02 18:19:48 2006 +0200
@@ -934,11 +934,10 @@
   apply (subst Rep_matrix_inject[symmetric])
   apply (rule ext)+
   apply (case_tac "j + int u < 0")
-  apply (simp, arith)
+  apply simp
   apply (case_tac "i + int v < 0")
-  apply (simp add: neg_def, arith)
   apply (simp add: neg_def)
-  apply arith
+  apply (simp add: neg_def)
   done
 
 lemma Rep_take_columns[simp]:
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