equal
deleted
inserted
replaced
6 Converted to Isar and polished by lcp |
6 Converted to Isar and polished by lcp |
7 *) |
7 *) |
8 |
8 |
9 header{*Completeness of the Reals; Floor and Ceiling Functions*} |
9 header{*Completeness of the Reals; Floor and Ceiling Functions*} |
10 |
10 |
11 theory RComplete = Lubs + RealDef: |
11 theory RComplete |
|
12 import Lubs RealDef |
|
13 begin |
12 |
14 |
13 lemma real_sum_of_halves: "x/2 + x/2 = (x::real)" |
15 lemma real_sum_of_halves: "x/2 + x/2 = (x::real)" |
14 by simp |
16 by simp |
15 |
17 |
16 |
18 |