NEWS
changeset 14255 e6e3e3f0deed
parent 14254 342634f38451
child 14257 a7ef3f7588c5
--- a/NEWS	Thu Nov 06 14:18:05 2003 +0100
+++ b/NEWS	Thu Nov 06 20:45:02 2003 +0100
@@ -56,6 +56,14 @@
 
 *** HOL ***
 
+* Records:
+  - Record types are now by default printed with their type abbreviation
+    instead of the list of all field types. This can be configured via
+    the reference "print_record_type_abbr".
+  - Simproc "record_upd_simproc" for simplification of multiple updates added 
+    (not enabled by default).
+  - Tactic "record_split_simp_tac" to split and simplify records added.
+ 
 * 'specification' command added, allowing for definition by
   specification.  There is also an 'ax_specification' command that
   introduces the new constants axiomatically.