# 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)
 --------------------------------