* HOL/record: cases/induct for more parts;
authorwenzelm
Tue, 20 Nov 2001 22:53:05 +0100
changeset 12253 1886dc96b7e9
parent 12252 835fef0fac51
child 12254 78bc1f3462b5
* HOL/record: cases/induct for more parts; * syntax: prefer later print_translation functions;
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;