author | wenzelm |
Sat, 29 May 2004 16:47:06 +0200 | |
changeset 14846 | b1fcade3880b |
parent 14387 | e96d5c42c4b0 |
child 15131 | c69542757a4d |
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 |
||
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
13957
diff
changeset
|
8 |
theory ComplexBin = Complex: |
13957 | 9 |