src/HOL/Matrix/Matrix.thy
changeset 23879 4776af8be741
parent 23477 f4b83f03cac9
child 25303 0699e20feabd
     1.1 --- a/src/HOL/Matrix/Matrix.thy	Fri Jul 20 14:27:56 2007 +0200
     1.2 +++ b/src/HOL/Matrix/Matrix.thy	Fri Jul 20 14:28:01 2007 +0200
     1.3 @@ -22,8 +22,10 @@
     1.4  instance matrix :: ("{plus, times, zero}") times
     1.5    times_matrix_def: "A * B \<equiv> mult_matrix (op *) (op +) A B" ..
     1.6  
     1.7 +instance matrix :: (lordered_ab_group) abs
     1.8 +  abs_matrix_def: "abs A \<equiv> sup A (- A)" ..
     1.9 +
    1.10  instance matrix :: (lordered_ab_group) lordered_ab_group_meet
    1.11 -  abs_matrix_def: "abs (A::('a::lordered_ab_group) matrix) == sup A (- A)"
    1.12  proof 
    1.13    fix A B C :: "('a::lordered_ab_group) matrix"
    1.14    show "A + B + C = A + (B + C)"