equal
deleted
inserted
replaced
1 (* Title : NSCA.thy |
1 (* Title : NSA/NSCA.thy |
2 Author : Jacques D. Fleuriot |
2 Author : Jacques D. Fleuriot |
3 Copyright : 2001,2002 University of Edinburgh |
3 Copyright : 2001,2002 University of Edinburgh |
4 *) |
4 *) |
5 |
5 |
6 header{*Non-Standard Complex Analysis*} |
6 header{*Non-Standard Complex Analysis*} |
7 |
7 |
8 theory NSCA |
8 theory NSCA |
9 imports NSComplex "../Hyperreal/HTranscendental" |
9 imports NSComplex HTranscendental |
10 begin |
10 begin |
11 |
11 |
12 abbreviation |
12 abbreviation |
13 (* standard complex numbers reagarded as an embedded subset of NS complex *) |
13 (* standard complex numbers reagarded as an embedded subset of NS complex *) |
14 SComplex :: "hcomplex set" where |
14 SComplex :: "hcomplex set" where |