--- a/src/HOL/Matrix/Matrix.thy Mon Jul 14 17:51:48 2008 +0200
+++ b/src/HOL/Matrix/Matrix.thy Mon Jul 14 19:20:28 2008 +0200
@@ -1286,7 +1286,7 @@
apply (rule ext)+
by simp
-instantiation matrix :: ("{ord, zero}") ord
+instantiation matrix :: ("{zero, ord}") ord
begin
definition
@@ -1299,7 +1299,7 @@
end
-instance matrix :: ("{order, zero}") order
+instance matrix :: ("{zero, order}") order
apply intro_classes
apply (simp_all add: le_matrix_def less_def)
apply (auto)
@@ -1437,7 +1437,7 @@
apply (auto)
done
-instantiation matrix :: ("{zero, lattice}") lattice
+instantiation matrix :: ("{lattice, zero}") lattice
begin
definition [code func del]: "inf = combine_matrix inf"