author | kleing |
Tue, 23 Dec 2003 06:35:41 +0100 | |
changeset 14316 | 91b897b9a2dc |
parent 13957 | 10dbf16be15f |
permissions | -rw-r--r-- |
13957 | 1 |
(* Title: NSComplexBin.thy |
2 |
Author: Jacques D. Fleuriot |
|
3 |
Copyright: 2001 University of Edinburgh |
|
4 |
Descrition: Binary arithmetic for the nonstandard complex numbers |
|
5 |
This case is reduced to that for the complexes (hence reals). |
|
6 |
*) |
|
7 |
||
8 |
NSComplexBin = NSComplex + |
|
9 |
||
10 |
||
11 |
instance |
|
12 |
hcomplex :: number |
|
13 |
||
14 |
defs |
|
15 |
hcomplex_number_of_def |
|
16 |
"number_of v == hcomplex_of_complex (number_of v)" |
|
17 |
(*::bin=>complex ::bin=>complex*) |
|
18 |
||
19 |
end |