1.1 --- a/NEWS	Thu Nov 06 14:18:05 2003 +0100
     1.2 +++ b/NEWS	Thu Nov 06 20:45:02 2003 +0100
     1.3 @@ -56,6 +56,14 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Records:
     1.8 +  - Record types are now by default printed with their type abbreviation
     1.9 +    instead of the list of all field types. This can be configured via
    1.10 +    the reference "print_record_type_abbr".
    1.11 +  - Simproc "record_upd_simproc" for simplification of multiple updates added 
    1.12 +    (not enabled by default).
    1.13 +  - Tactic "record_split_simp_tac" to split and simplify records added.
    1.14 + 
    1.15  * 'specification' command added, allowing for definition by
    1.16    specification.  There is also an 'ax_specification' command that
    1.17    introduces the new constants axiomatically.