src/HOL/Matrix/Matrix.thy
changeset 28562 4e74209f113e
parent 27653 180e28bab764
child 28637 7aabaf1ba263
     1.1 --- a/src/HOL/Matrix/Matrix.thy	Fri Oct 10 06:45:50 2008 +0200
     1.2 +++ b/src/HOL/Matrix/Matrix.thy	Fri Oct 10 06:45:53 2008 +0200
     1.3 @@ -768,7 +768,7 @@
     1.4  instantiation matrix :: (zero) zero
     1.5  begin
     1.6  
     1.7 -definition zero_matrix_def [code func del]: "0 = Abs_matrix (\<lambda>j i. 0)"
     1.8 +definition zero_matrix_def [code del]: "0 = Abs_matrix (\<lambda>j i. 0)"
     1.9  
    1.10  instance ..
    1.11  
    1.12 @@ -1440,9 +1440,9 @@
    1.13  instantiation matrix :: ("{lattice, zero}") lattice
    1.14  begin
    1.15  
    1.16 -definition [code func del]: "inf = combine_matrix inf"
    1.17 +definition [code del]: "inf = combine_matrix inf"
    1.18  
    1.19 -definition [code func del]: "sup = combine_matrix sup"
    1.20 +definition [code del]: "sup = combine_matrix sup"
    1.21  
    1.22  instance
    1.23    by default (auto simp add: inf_le1 inf_le2 le_infI le_matrix_def inf_matrix_def sup_matrix_def)
    1.24 @@ -1453,7 +1453,7 @@
    1.25  begin
    1.26  
    1.27  definition
    1.28 -  plus_matrix_def [code func del]: "A + B = combine_matrix (op +) A B"
    1.29 +  plus_matrix_def [code del]: "A + B = combine_matrix (op +) A B"
    1.30  
    1.31  instance ..
    1.32  
    1.33 @@ -1463,7 +1463,7 @@
    1.34  begin
    1.35  
    1.36  definition
    1.37 -  minus_matrix_def [code func del]: "- A = apply_matrix uminus A"
    1.38 +  minus_matrix_def [code del]: "- A = apply_matrix uminus A"
    1.39  
    1.40  instance ..
    1.41  
    1.42 @@ -1473,7 +1473,7 @@
    1.43  begin
    1.44  
    1.45  definition
    1.46 -  diff_matrix_def [code func del]: "A - B = combine_matrix (op -) A B"
    1.47 +  diff_matrix_def [code del]: "A - B = combine_matrix (op -) A B"
    1.48  
    1.49  instance ..
    1.50  
    1.51 @@ -1483,7 +1483,7 @@
    1.52  begin
    1.53  
    1.54  definition
    1.55 -  times_matrix_def [code func del]: "A * B = mult_matrix (op *) (op +) A B"
    1.56 +  times_matrix_def [code del]: "A * B = mult_matrix (op *) (op +) A B"
    1.57  
    1.58  instance ..
    1.59  
    1.60 @@ -1493,7 +1493,7 @@
    1.61  begin
    1.62  
    1.63  definition
    1.64 -  abs_matrix_def [code func del]: "abs (A \<Colon> 'a matrix) = sup A (- A)"
    1.65 +  abs_matrix_def [code del]: "abs (A \<Colon> 'a matrix) = sup A (- A)"
    1.66  
    1.67  instance ..
    1.68