equal
deleted
inserted
replaced
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 |
9 imports NSComplex "../Hyperreal/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 |