author | wenzelm |
Tue, 13 Dec 2005 19:32:05 +0100 | |
changeset 18398 | 5d63a8b35688 |
parent 15140 | 322485b816ac |
permissions | -rw-r--r-- |
13957 | 1 |
(* Title: ComplexBin.thy |
2 |
Author: Jacques D. Fleuriot |
|
3 |
Copyright: 2001 University of Edinburgh |
|
4 |
Descrition: Binary arithmetic for the complex numbers |
|
5 |
This case is reduced to that for the reals. |
|
6 |
*) |
|
7 |
||
15131 | 8 |
theory ComplexBin |
15140 | 9 |
imports Complex |
15131 | 10 |
begin |
13957 | 11 |
|
15131 | 12 |
end |
13 |