| changeset 5106 | 05b7c9a2ddf9 |
| parent 5085 | 8e5a7942fdea |
| child 5109 | b3d18eb3ac20 |
--- 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);