1
(* Title : RComplete.thy
2
ID : $Id$
3
Author : Jacques D. Fleuriot
4
Copyright : 1998 University of Cambridge
5
Description : Completeness theorems for positive
6
reals and reals
7
*)
8
9
RComplete = Lubs + RealArith
10