| changeset 22983 | 3314057c3b57 |
| parent 17635 | 9234108fdfb1 |
| child 26121 | d4fbf84a6636 |
| 22982:bff3fcdeecd3 | 22983:3314057c3b57 |
|---|---|
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 |
10 theory Hyperreal |
11 imports Poly Taylor HLog |
11 imports Ln Poly Taylor Integration HLog |
12 begin |
12 begin |
13 |
13 |
14 end |
14 end |