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 