| changeset 28944 | e27abf0db984 |
| parent 26311 | 81a0fc28b0de |
| 28943:9fb44eb4425d | 28944:e27abf0db984 |
|---|---|
6 *) |
6 *) |
7 |
7 |
8 header {* Complex Numbers: Rectangular and Polar Representations *} |
8 header {* Complex Numbers: Rectangular and Polar Representations *} |
9 |
9 |
10 theory Complex |
10 theory Complex |
11 imports "../Real/Real" "../Hyperreal/Transcendental" |
11 imports "../Hyperreal/Transcendental" |
12 begin |
12 begin |
13 |
13 |
14 datatype complex = Complex real real |
14 datatype complex = Complex real real |
15 |
15 |
16 primrec |
16 primrec |