--- a/src/HOL/Matrix/MatrixGeneral.thy Wed Feb 02 09:15:40 2005 +0100
+++ b/src/HOL/Matrix/MatrixGeneral.thy Wed Feb 02 10:16:33 2005 +0100
@@ -41,8 +41,7 @@
from hyp have d: "Max (?S) < m" by (simp add: a nrows_def)
have "m \<notin> ?S"
proof -
- have "m \<in> ?S \<Longrightarrow> m <= Max(?S)" by (simp add:Max_le[OF
- c b])
+ have "m \<in> ?S \<Longrightarrow> m <= Max(?S)" by (simp add:Max_ge[OF c b])
moreover from d have "~(m <= Max ?S)" by (simp)
ultimately show "m \<notin> ?S" by (auto)
qed