# HG changeset patch
# User wenzelm
# Date 1006293185 -3600
# Node ID 1886dc96b7e963a027443dd50fec7d566aab1a68
# Parent  835fef0fac51ef9e959c56a1814b150353bda24a
* HOL/record: cases/induct for more parts;
* syntax: prefer later print_translation functions;

diff -r 835fef0fac51 -r 1886dc96b7e9 NEWS
--- a/NEWS	Tue Nov 20 20:57:46 2001 +0100
+++ b/NEWS	Tue Nov 20 22:53:05 2001 +0100
@@ -155,7 +155,9 @@
 * HOL/record:
   - removed old "make" and "make_scheme" operations -- INCOMPATIBILITY;
   - removed "more" class (simply use "term") -- INCOMPATIBILITY;
-  - provides cases/induct rules for use with corresponding Isar methods;
+  - provides cases/induct rules for use with corresponding Isar
+    methods (for concrete records, record schemes, concrete more
+    parts, schematic more parts -- in that order);
   - new derived operations "make" (for adding fields of current
     record), "extend" to promote fixed record to record scheme, and
     "truncate" for the reverse; cf. theorems "derived_defs", which are
@@ -246,6 +248,10 @@
 * syntax: builtin parse translation for "_constify" turns valued
 tokens into AST constants;
 
+* syntax: prefer later print_translation functions; potential
+INCOMPATIBILITY: need to reverse declarations of multiple translation
+functions for same constant;
+
 * system: refrain from any attempt at filtering input streams; no
 longer support ``8bit'' encoding of old isabelle font, instead proper
 iso-latin characters may now be used;