src/HOL/Matrix/Matrix.thy
changeset 17915 e38947f9ba5e
parent 16733 236dfafbeb63
child 20633 e98f59806244
     1.1 --- a/src/HOL/Matrix/Matrix.thy	Wed Oct 19 21:52:07 2005 +0200
     1.2 +++ b/src/HOL/Matrix/Matrix.thy	Wed Oct 19 21:52:27 2005 +0200
     1.3 @@ -3,16 +3,15 @@
     1.4      Author:     Steven Obua
     1.5  *)
     1.6  
     1.7 -theory Matrix=MatrixGeneral:
     1.8 -
     1.9 -instance matrix :: (minus) minus 
    1.10 -by intro_classes
    1.11 +theory Matrix
    1.12 +imports MatrixGeneral
    1.13 +begin
    1.14  
    1.15 -instance matrix :: (plus) plus
    1.16 -by (intro_classes)
    1.17 +instance matrix :: (minus) minus ..
    1.18  
    1.19 -instance matrix :: ("{plus,times}") times
    1.20 -by (intro_classes)
    1.21 +instance matrix :: (plus) plus ..
    1.22 +
    1.23 +instance matrix :: ("{plus,times}") times ..
    1.24  
    1.25  defs (overloaded)
    1.26    plus_matrix_def: "A + B == combine_matrix (op +) A B"