equal
deleted
inserted
replaced
1 (* Title: HOL/Matrix/Matrix.thy |
1 (* Title: HOL/Matrix/Matrix.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Steven Obua |
3 Author: Steven Obua |
4 *) |
4 *) |
5 |
5 |
6 theory Matrix=MatrixGeneral: |
6 theory Matrix |
7 |
7 imports MatrixGeneral |
8 instance matrix :: (minus) minus |
8 begin |
9 by intro_classes |
9 |
10 |
10 instance matrix :: (minus) minus .. |
11 instance matrix :: (plus) plus |
11 |
12 by (intro_classes) |
12 instance matrix :: (plus) plus .. |
13 |
13 |
14 instance matrix :: ("{plus,times}") times |
14 instance matrix :: ("{plus,times}") times .. |
15 by (intro_classes) |
|
16 |
15 |
17 defs (overloaded) |
16 defs (overloaded) |
18 plus_matrix_def: "A + B == combine_matrix (op +) A B" |
17 plus_matrix_def: "A + B == combine_matrix (op +) A B" |
19 diff_matrix_def: "A - B == combine_matrix (op -) A B" |
18 diff_matrix_def: "A - B == combine_matrix (op -) A B" |
20 minus_matrix_def: "- A == apply_matrix uminus A" |
19 minus_matrix_def: "- A == apply_matrix uminus A" |