Pure: considerably improved version of 'constdefs' command;
authorwenzelm
Thu Apr 22 12:19:40 2004 +0200 (2004-04-22)
changeset 146558a95abf87dd3
parent 14654 aad262a36014
child 14656 765badface6a
Pure: considerably improved version of 'constdefs' command;
Pure: 'advanced' translation functions (parse_translation etc.);
NEWS
     1.1 --- a/NEWS	Thu Apr 22 12:18:23 2004 +0200
     1.2 +++ b/NEWS	Thu Apr 22 12:19:40 2004 +0200
     1.3 @@ -1,6 +1,25 @@
     1.4  Isabelle NEWS -- history user-relevant changes
     1.5  ==============================================
     1.6  
     1.7 +New in this Isabelle release
     1.8 +----------------------------
     1.9 +
    1.10 +*** General ***
    1.11 +
    1.12 +* Pure: considerably improved version of 'constdefs' command.  Now
    1.13 +performs automatic type-inference of declared constants; additional
    1.14 +support for local structure declarations (cf. locales and HOL
    1.15 +records), see also isar-ref manual.  Potential INCOMPATIBILITY: need
    1.16 +to observe strictly sequential dependencies of definitions within a
    1.17 +single 'constdefs' section -- some existing specifications may have to
    1.18 +be reordered.
    1.19 +
    1.20 +* Pure: 'advanced' translation functions (parse_translation etc.) may
    1.21 +depend on the signature of the theory context being presently used for
    1.22 +parsing/printing, see also isar-ref manual.
    1.23 +
    1.24 +
    1.25 +
    1.26  New in Isabelle2004 (April 2004)
    1.27  --------------------------------
    1.28