equal
deleted
inserted
replaced
6 Construction of the Reals using Dedekind Cuts |
6 Construction of the Reals using Dedekind Cuts |
7 by Jacques Fleuriot |
7 by Jacques Fleuriot |
8 *) |
8 *) |
9 |
9 |
10 time_use_thy "Real"; |
10 time_use_thy "Real"; |
|
11 use_thy "Float"; |