* HOL/record: cases/induct for more parts;
authorwenzelm
Tue Nov 20 22:53:05 2001 +0100 (2001-11-20)
changeset 122531886dc96b7e9
parent 12252 835fef0fac51
child 12254 78bc1f3462b5
* HOL/record: cases/induct for more parts;
* syntax: prefer later print_translation functions;
NEWS
     1.1 --- a/NEWS	Tue Nov 20 20:57:46 2001 +0100
     1.2 +++ b/NEWS	Tue Nov 20 22:53:05 2001 +0100
     1.3 @@ -155,7 +155,9 @@
     1.4  * HOL/record:
     1.5    - removed old "make" and "make_scheme" operations -- INCOMPATIBILITY;
     1.6    - removed "more" class (simply use "term") -- INCOMPATIBILITY;
     1.7 -  - provides cases/induct rules for use with corresponding Isar methods;
     1.8 +  - provides cases/induct rules for use with corresponding Isar
     1.9 +    methods (for concrete records, record schemes, concrete more
    1.10 +    parts, schematic more parts -- in that order);
    1.11    - new derived operations "make" (for adding fields of current
    1.12      record), "extend" to promote fixed record to record scheme, and
    1.13      "truncate" for the reverse; cf. theorems "derived_defs", which are
    1.14 @@ -246,6 +248,10 @@
    1.15  * syntax: builtin parse translation for "_constify" turns valued
    1.16  tokens into AST constants;
    1.17  
    1.18 +* syntax: prefer later print_translation functions; potential
    1.19 +INCOMPATIBILITY: need to reverse declarations of multiple translation
    1.20 +functions for same constant;
    1.21 +
    1.22  * system: refrain from any attempt at filtering input streams; no
    1.23  longer support ``8bit'' encoding of old isabelle font, instead proper
    1.24  iso-latin characters may now be used;