HOL-Real
authorpaulson
Wed Jul 01 17:59:25 1998 +0200 (1998-07-01)
changeset 510605b7c9a2ddf9
parent 5105 0ff5bec04d02
child 5107 2edf5dfb02f3
HOL-Real
NEWS
     1.1 --- a/NEWS	Wed Jul 01 11:33:39 1998 +0200
     1.2 +++ b/NEWS	Wed Jul 01 17:59:25 1998 +0200
     1.3 @@ -46,6 +46,8 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* HOL/Real: a construction of the reals using Dedekind cuts
     1.8 +
     1.9  * HOL/record: now includes concrete syntax for record terms (still
    1.10  lacks important theorems, like surjective pairing and split);
    1.11