| changeset 15131 | c69542757a4d |
| parent 14387 | e96d5c42c4b0 |
| child 15140 | 322485b816ac |
| 15130:dc6be28d7f4e | 15131:c69542757a4d |
|---|---|
3 Copyright: 2001 University of Edinburgh |
3 Copyright: 2001 University of Edinburgh |
4 Descrition: Binary arithmetic for the complex numbers |
4 Descrition: Binary arithmetic for the complex numbers |
5 This case is reduced to that for the reals. |
5 This case is reduced to that for the reals. |
6 *) |
6 *) |
7 |
7 |
8 theory ComplexBin = Complex: |
8 theory ComplexBin |
9 import Complex |
|
10 begin |
|
9 |
11 |
12 end |
|
13 |