improved handling of "that": insert into goal, only declare as Pure "intro";
eliminated functor;
(* 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