diff -r 056255ade52a -r 4e74209f113e src/HOL/Matrix/Matrix.thy
--- 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 ..