* HOL: syntax translations now work properly with numerals and records
authorwenzelm
Wed Aug 08 17:37:47 2001 +0200 (2001-08-08)
changeset 1148795071c9e85a3
parent 11486 8f32860eac3a
child 11488 4ff900551340
* HOL: syntax translations now work properly with numerals and records
expressions;
NEWS
     1.1 --- a/NEWS	Wed Aug 08 16:57:43 2001 +0200
     1.2 +++ b/NEWS	Wed Aug 08 17:37:47 2001 +0200
     1.3 @@ -21,8 +21,8 @@
     1.4    relations has too general a domain, namely ('a * 'b)set and 'a => 'b.
     1.5    This means that it may be necessary to attach explicit type constraints.
     1.6  
     1.7 -* HOL records: fix problem with user translations by making field
     1.8 -names appear as syntactic conststants;
     1.9 +* HOL: syntax translations now work properly with numerals and records
    1.10 +expressions;
    1.11  
    1.12  * HOL/GroupTheory: group theory examples including Sylow's theorem, by
    1.13  Florian Kammüller;