(* Title : RComplete.thy Author : Jacques D. Fleuriot Copyright : 1998 University of Cambridge Description : Completeness theorems for positive reals and reals *) RComplete = Lubs + Real