# HG changeset patch
# User nipkow
# Date 1107335793 -3600
# Node ID e93a3badc2bc49b96d1defc9c5677455f94321b1
# Parent  2636ec211ec841f96c2267f823fdd379ce672fe6
Max_le -> Max_ge

diff -r 2636ec211ec8 -r e93a3badc2bc src/HOL/Matrix/MatrixGeneral.thy
--- 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