(*  Title       : RComplete.thy
    ID          : $Id: RComplete.thy,v 1.3 1999/08/19 16:36:42 paulson Exp $
    Author      : Jacques D. Fleuriot
    Copyright   : 1998  University of Cambridge
    Description : Completeness theorems for positive
                  reals and reals 
*) 

RComplete = Lubs + RealBin