Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Matrix/MatrixGeneral.thy
changeset 20283 81b7832b29a3
parent 20217 25b068a99d2b
child 20432 07ec57376051 
--- 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]:
isabelle