src/HOL/Real/RComplete.thy
changeset 15140 322485b816ac
parent 15131 c69542757a4d
child 15234 ec91a90c604e
equal deleted inserted replaced
15139:58cd3404cf75 15140:322485b816ac
     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
    11 theory RComplete
    12 import Lubs RealDef
    12 imports Lubs RealDef
    13 begin
    13 begin
    14 
    14 
    15 lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"
    15 lemma real_sum_of_halves: "x/2 + x/2 = (x::real)"
    16 by simp
    16 by simp
    17 
    17