# HG changeset patch
# User haftmann
# Date 1174077134 -3600
# Node ID bd4379c9b4d0e6d80e7b80ef00c9002f8f2fcd94
# Parent  1ed5b9c3ae6737bc9f033e0f01514a838135a411
tuned

diff -r 1ed5b9c3ae67 -r bd4379c9b4d0 src/HOL/Matrix/MatrixGeneral.thy
--- a/src/HOL/Matrix/MatrixGeneral.thy	Fri Mar 16 21:32:13 2007 +0100
+++ b/src/HOL/Matrix/MatrixGeneral.thy	Fri Mar 16 21:32:14 2007 +0100
@@ -1274,11 +1274,9 @@
 apply (rule ext)+
 by simp
 
-instance matrix :: ("{ord, zero}") ord ..
-
-defs (overloaded)
-  le_matrix_def: "(A::('a::{ord,zero}) matrix) <= B == ! j i. (Rep_matrix A j i) <= (Rep_matrix B j i)"
-  less_def: "(A::('a::{ord,zero}) matrix) < B == (A <= B) & (A \<noteq> B)"
+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 \<equiv> A \<le> B \<and> A \<noteq> B" ..
 
 instance matrix :: ("{order, zero}") order
 apply intro_classes