# HG changeset patch # User wenzelm # Date 1082629180 -7200 # Node ID 8a95abf87dd3f1effd18676efa833fef253a47bb # Parent aad262a360146ef6393bd928e99085a6df6bb8b2 Pure: considerably improved version of 'constdefs' command; Pure: 'advanced' translation functions (parse_translation etc.); diff -r aad262a36014 -r 8a95abf87dd3 NEWS --- a/NEWS Thu Apr 22 12:18:23 2004 +0200 +++ b/NEWS Thu Apr 22 12:19:40 2004 +0200 @@ -1,6 +1,25 @@ Isabelle NEWS -- history user-relevant changes ============================================== +New in this Isabelle release +---------------------------- + +*** General *** + +* Pure: considerably improved version of 'constdefs' command. Now +performs automatic type-inference of declared constants; additional +support for local structure declarations (cf. locales and HOL +records), see also isar-ref manual. Potential INCOMPATIBILITY: need +to observe strictly sequential dependencies of definitions within a +single 'constdefs' section -- some existing specifications may have to +be reordered. + +* Pure: 'advanced' translation functions (parse_translation etc.) may +depend on the signature of the theory context being presently used for +parsing/printing, see also isar-ref manual. + + + New in Isabelle2004 (April 2004) --------------------------------