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