| changeset 15131 | c69542757a4d |
| parent 13958 | c1c67582c9b5 |
| child 15140 | 322485b816ac |
| 15130:dc6be28d7f4e | 15131:c69542757a4d |
|---|---|
5 |
5 |
6 Construction of the Hyperreals by the Ultrapower Construction |
6 Construction of the Hyperreals by the Ultrapower Construction |
7 and mechanization of Nonstandard Real Analysis |
7 and mechanization of Nonstandard Real Analysis |
8 *) |
8 *) |
9 |
9 |
10 theory Hyperreal = Poly + MacLaurin + HLog: |
10 theory Hyperreal |
11 import Poly MacLaurin HLog |
|
12 begin |
|
11 |
13 |
12 end |
14 end |