# HG changeset patch
# User wenzelm
# Date 997285067 -7200
# Node ID 95071c9e85a335438261395a1b5b4862d24e3701
# Parent  8f32860eac3afd89648e87303a0cd4d487d8ea2b
* HOL: syntax translations now work properly with numerals and records
expressions;

diff -r 8f32860eac3a -r 95071c9e85a3 NEWS
--- a/NEWS	Wed Aug 08 16:57:43 2001 +0200
+++ b/NEWS	Wed Aug 08 17:37:47 2001 +0200
@@ -21,8 +21,8 @@
   relations has too general a domain, namely ('a * 'b)set and 'a => 'b.
   This means that it may be necessary to attach explicit type constraints.
 
-* HOL records: fix problem with user translations by making field
-names appear as syntactic conststants;
+* HOL: syntax translations now work properly with numerals and records
+expressions;
 
 * HOL/GroupTheory: group theory examples including Sylow's theorem, by
 Florian Kammüller;