| changeset 7292 | dff3470c5c62 |
| parent 7218 | bfa767b4dc51 |
| child 9013 | 9dd0274f76af |
| 7291:8aa66ddc0bea | 7292:dff3470c5c62 |
|---|---|
3 Author : Jacques D. Fleuriot |
3 Author : Jacques D. Fleuriot |
4 Copyright : 1998 University of Cambridge |
4 Copyright : 1998 University of Cambridge |
5 Description : Construction of hyperreals using ultrafilters |
5 Description : Construction of hyperreals using ultrafilters |
6 *) |
6 *) |
7 |
7 |
8 HyperDef = Filter + Real + |
8 HyperDef = Filter + RealBin + |
9 |
9 |
10 consts |
10 consts |
11 |
11 |
12 FreeUltrafilterNat :: nat set set |
12 FreeUltrafilterNat :: nat set set |
13 |
13 |