reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
(* Title : RComplete.thy ID : $Id$ Author : Jacques D. Fleuriot Copyright : 1998 University of Cambridge Description : Completeness theorems for positive reals and reals *) RComplete = Lubs + RealArith