diff -r ca638d713ff8 -r b1d955791529 src/HOL/Matrix_LP/Matrix.thy
--- a/src/HOL/Matrix_LP/Matrix.thy	Thu Oct 31 16:54:22 2013 +0100
+++ b/src/HOL/Matrix_LP/Matrix.thy	Fri Nov 01 18:51:14 2013 +0100
@@ -1542,8 +1542,8 @@
   fix A B :: "'a matrix"
   show "- A + A = 0" 
     by (simp add: plus_matrix_def minus_matrix_def Rep_matrix_inject[symmetric] ext)
-  show "A - B = A + - B"
-    by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject [symmetric] ext diff_minus)
+  show "A + - B = A - B"
+    by (simp add: plus_matrix_def diff_matrix_def minus_matrix_def Rep_matrix_inject [symmetric] ext)
 qed
 
 instance matrix :: (ab_group_add) ab_group_add