src/HOL/Matrix/MatrixGeneral.thy
changeset 25764 878c37886eed
parent 25502 9200b36280c0
child 26304 02fbd0e7954a
--- 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