| changeset 25502 | 9200b36280c0 |
| parent 23373 | ead82c82da9e |
| child 25764 | 878c37886eed |
--- a/src/HOL/Matrix/MatrixGeneral.thy Thu Nov 29 07:55:46 2007 +0100 +++ b/src/HOL/Matrix/MatrixGeneral.thy Thu Nov 29 17:08:26 2007 +0100 @@ -1281,7 +1281,7 @@ 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" .. + less_def: "A < (B\<Colon>'a matrix) \<equiv> A \<le> B \<and> A \<noteq> B" .. instance matrix :: ("{order, zero}") order apply intro_classes