| changeset 51518 | 6a56b7088a6a |
| parent 49962 | a8cc904a6820 |
| child 51519 | 2831ce75ec49 |
| 51517:7957d26c3334 | 51518:6a56b7088a6a |
|---|---|
6 *) |
6 *) |
7 |
7 |
8 header {* Completeness of the Reals; Floor and Ceiling Functions *} |
8 header {* Completeness of the Reals; Floor and Ceiling Functions *} |
9 |
9 |
10 theory RComplete |
10 theory RComplete |
11 imports Lubs RealDef |
11 imports Conditional_Complete_Lattices RealDef |
12 begin |
12 begin |
13 |
13 |
14 lemma real_sum_of_halves: "x/2 + x/2 = (x::real)" |
14 lemma real_sum_of_halves: "x/2 + x/2 = (x::real)" |
15 by simp |
15 by simp |
16 |
16 |