| changeset 58878 | f962e42e324d |
| parent 58787 | af9eb5e566dd |
| child 59658 | 0cc388370041 |
| 58877:262572d90bc6 | 58878:f962e42e324d |
|---|---|
1 (* Title: HOL/NSA/NSComplex.thy |
1 (* Title: HOL/NSA/NSComplex.thy |
2 Author: Jacques D. Fleuriot, University of Edinburgh |
2 Author: Jacques D. Fleuriot, University of Edinburgh |
3 Author: Lawrence C Paulson |
3 Author: Lawrence C Paulson |
4 *) |
4 *) |
5 |
5 |
6 header{*Nonstandard Complex Numbers*} |
6 section{*Nonstandard Complex Numbers*} |
7 |
7 |
8 theory NSComplex |
8 theory NSComplex |
9 imports NSA |
9 imports NSA |
10 begin |
10 begin |
11 |
11 |