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