HOL-Real

--- a/NEWS	Wed Jul 01 11:33:39 1998 +0200
+++ b/NEWS	Wed Jul 01 17:59:25 1998 +0200
@@ -46,6 +46,8 @@
 
 *** HOL ***
 
+* HOL/Real: a construction of the reals using Dedekind cuts
+
 * HOL/record: now includes concrete syntax for record terms (still
 lacks important theorems, like surjective pairing and split);