--- a/src/HOL/Matrix/MatrixGeneral.thy Wed Jan 02 15:14:15 2008 +0100
+++ b/src/HOL/Matrix/MatrixGeneral.thy Wed Jan 02 15:14:17 2008 +0100
@@ -1279,9 +1279,18 @@
apply (rule ext)+
by simp
-instance matrix :: ("{ord, zero}") ord
- le_matrix_def: "A \<le> B \<equiv> \<forall>j i. Rep_matrix A j i \<le> Rep_matrix B j i"
- less_def: "A < (B\<Colon>'a matrix) \<equiv> A \<le> B \<and> A \<noteq> B" ..
+instantiation matrix :: ("{ord, zero}") ord
+begin
+
+definition
+ le_matrix_def: "A \<le> B \<longleftrightarrow> (\<forall>j i. Rep_matrix A j i \<le> Rep_matrix B j i)"
+
+definition
+ less_def: "A < (B\<Colon>'a matrix) \<longleftrightarrow> A \<le> B \<and> A \<noteq> B"
+
+instance ..
+
+end
instance matrix :: ("{order, zero}") order
apply intro_classes