diff -r 5daa82ba4078 -r dcbe9f756ae0 src/HOL/Matrix_LP/Matrix.thy
--- a/src/HOL/Matrix_LP/Matrix.thy	Mon Dec 07 10:49:08 2015 +0100
+++ b/src/HOL/Matrix_LP/Matrix.thy	Thu Dec 10 13:38:40 2015 +0000
@@ -875,7 +875,7 @@
 apply (subst RepAbs_matrix)
 apply auto
 apply (simp add: Suc_le_eq)
-apply (rule not_leE)
+apply (rule not_le_imp_less)
 apply (subst nrows_le)
 by simp
 qed
@@ -891,7 +891,7 @@
 apply (subst RepAbs_matrix)
 apply auto
 apply (simp add: Suc_le_eq)
-apply (rule not_leE)
+apply (rule not_le_imp_less)
 apply (subst ncols_le)
 by simp
 qed