| changeset 41959 | b460124855b8 |
| parent 41413 | 64cd30d6b0b8 |
| child 42463 | f270e3e18be5 |
| 41958:5abc60a017e0 | 41959:b460124855b8 |
|---|---|
1 (* Title: NSComplex.thy |
1 (* Title: HOL/NSA/NSComplex.thy |
2 Author: Jacques D. Fleuriot |
2 Author: Jacques D. Fleuriot, University of Edinburgh |
3 Copyright: 2001 University of Edinburgh |
3 Author: Lawrence C Paulson |
4 Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4 |
|
5 *) |
4 *) |
6 |
5 |
7 header{*Nonstandard Complex Numbers*} |
6 header{*Nonstandard Complex Numbers*} |
8 |
7 |
9 theory NSComplex |
8 theory NSComplex |