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