| changeset 27468 | 0783dd1dc13d |
| child 28952 | 15a4b2cf8c34 |
| 27467:c0c4a6bd2cbc | 27468:0783dd1dc13d |
|---|---|
1 (* Title: HOL/Hyperreal/Hyperreal.thy |
|
2 ID: $Id$ |
|
3 Author: Jacques Fleuriot, Cambridge University Computer Laboratory |
|
4 Copyright 1998 University of Cambridge |
|
5 |
|
6 Construction of the Hyperreals by the Ultrapower Construction |
|
7 and mechanization of Nonstandard Real Analysis |
|
8 *) |
|
9 |
|
10 theory Hyperreal |
|
11 imports Ln Deriv Taylor Integration HLog |
|
12 begin |
|
13 |
|
14 end |