--- a/src/HOL/Matrix_LP/Matrix.thy Tue Sep 01 17:25:36 2015 +0200
+++ b/src/HOL/Matrix_LP/Matrix.thy Tue Sep 01 22:32:58 2015 +0200
@@ -1290,7 +1290,7 @@
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> \<not> B \<le> A"
+ less_def: "A < (B::'a matrix) \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> A"
instance ..
@@ -1496,7 +1496,7 @@
begin
definition
- abs_matrix_def: "abs (A \<Colon> 'a matrix) = sup A (- A)"
+ abs_matrix_def: "abs (A :: 'a matrix) = sup A (- A)"
instance ..