--- a/src/HOL/Matrix/Matrix.thy Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Matrix/Matrix.thy Fri Oct 10 06:45:53 2008 +0200
@@ -768,7 +768,7 @@
instantiation matrix :: (zero) zero
begin
-definition zero_matrix_def [code func del]: "0 = Abs_matrix (\<lambda>j i. 0)"
+definition zero_matrix_def [code del]: "0 = Abs_matrix (\<lambda>j i. 0)"
instance ..
@@ -1440,9 +1440,9 @@
instantiation matrix :: ("{lattice, zero}") lattice
begin
-definition [code func del]: "inf = combine_matrix inf"
+definition [code del]: "inf = combine_matrix inf"
-definition [code func del]: "sup = combine_matrix sup"
+definition [code del]: "sup = combine_matrix sup"
instance
by default (auto simp add: inf_le1 inf_le2 le_infI le_matrix_def inf_matrix_def sup_matrix_def)
@@ -1453,7 +1453,7 @@
begin
definition
- plus_matrix_def [code func del]: "A + B = combine_matrix (op +) A B"
+ plus_matrix_def [code del]: "A + B = combine_matrix (op +) A B"
instance ..
@@ -1463,7 +1463,7 @@
begin
definition
- minus_matrix_def [code func del]: "- A = apply_matrix uminus A"
+ minus_matrix_def [code del]: "- A = apply_matrix uminus A"
instance ..
@@ -1473,7 +1473,7 @@
begin
definition
- diff_matrix_def [code func del]: "A - B = combine_matrix (op -) A B"
+ diff_matrix_def [code del]: "A - B = combine_matrix (op -) A B"
instance ..
@@ -1483,7 +1483,7 @@
begin
definition
- times_matrix_def [code func del]: "A * B = mult_matrix (op *) (op +) A B"
+ times_matrix_def [code del]: "A * B = mult_matrix (op *) (op +) A B"
instance ..
@@ -1493,7 +1493,7 @@
begin
definition
- abs_matrix_def [code func del]: "abs (A \<Colon> 'a matrix) = sup A (- A)"
+ abs_matrix_def [code del]: "abs (A \<Colon> 'a matrix) = sup A (- A)"
instance ..