equal
deleted
inserted
replaced
5 |
5 |
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 no_document time_use_thy "Ring_and_Field"; |
|
11 time_use_thy "Real"; |
10 time_use_thy "Real"; |