| changeset 62479 | 716336f19aa9 |
| parent 51525 | d3d170a2887f |
| 62478:a62c86d25024 | 62479:716336f19aa9 |
|---|---|
1 (* Title: HOL/Nonstandard_Analysis/Hyperreal.thy |
|
2 Author: Jacques Fleuriot, Cambridge University Computer Laboratory |
|
3 Copyright 1998 University of Cambridge |
|
4 |
|
5 Construction of the Hyperreals by the Ultrapower Construction |
|
6 and mechanization of Nonstandard Real Analysis |
|
7 *) |
|
8 |
|
9 theory Hyperreal |
|
10 imports HLog |
|
11 begin |
|
12 |
|
13 end |