| changeset 15140 | 322485b816ac |
| parent 15131 | c69542757a4d |
| 15139:58cd3404cf75 | 15140:322485b816ac |
|---|---|
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 |
8 theory ComplexBin |
9 import Complex |
9 imports Complex |
10 begin |
10 begin |
11 |
11 |
12 end |
12 end |
13 |
13 |