| changeset 61824 | dcbe9f756ae0 |
| parent 61260 | e6f03fae14d5 |
| child 61945 | 1135b8de26c3 |
--- 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