| changeset 15140 | 322485b816ac |
| parent 15131 | c69542757a4d |
| child 15169 | 2b5da07a0b89 |
| 15139:58cd3404cf75 | 15140:322485b816ac |
|---|---|
6 *) |
6 *) |
7 |
7 |
8 header{*Nonstandard Complex Numbers*} |
8 header{*Nonstandard Complex Numbers*} |
9 |
9 |
10 theory NSComplex |
10 theory NSComplex |
11 import Complex |
11 imports Complex |
12 begin |
12 begin |
13 |
13 |
14 constdefs |
14 constdefs |
15 hcomplexrel :: "((nat=>complex)*(nat=>complex)) set" |
15 hcomplexrel :: "((nat=>complex)*(nat=>complex)) set" |
16 "hcomplexrel == {p. \<exists>X Y. p = ((X::nat=>complex),Y) & |
16 "hcomplexrel == {p. \<exists>X Y. p = ((X::nat=>complex),Y) & |