diff -r 757dac39c579 -r 8fa551e22e52 NEWS
--- a/NEWS	Wed Oct 20 00:09:36 1999 +0200
+++ b/NEWS	Wed Oct 20 11:05:06 1999 +0200
@@ -59,9 +59,14 @@
 tactical theorem proving; together with the ProofGeneral/isar user
 interface it offers an interactive environment for developing human
 readable proof documents (Isar == Intelligible semi-automated
-reasoning); actual document preparation based on (PDF)LaTeX is
-available as well; see isatool doc isar-ref, HOL/Isar_examples and
-http://isabelle.in.tum.de/Isar/ for more information.
+reasoning); for further information see isatool doc isar-ref,
+src/HOL/Isar_examples and http://isabelle.in.tum.de/Isar/;
+
+* improved presentation of theories: better HTML markup (including
+colors), graph views in several sizes; isatool usedir now provides a
+proper interface for user theories (via -P option); actual document
+preparation based on (PDF)LaTeX is available as well (for new-style
+theories only); see isatool doc system for more information;
 
 * native support for Proof General, both for classic Isabelle and
 Isabelle/Isar (the latter is slightly better supported and more
@@ -72,10 +77,6 @@
 
 * Isabelle manuals now also available as PDF;
 
-* improved browser info generation: better HTML markup (including
-colors), graph views in several sizes; isatool usedir now provides a
-proper interface for user theories (via -P option);
-
 * theory loader rewritten from scratch (may not be fully
 bug-compatible); old loadpath variable has been replaced by show_path,
 add_path, del_path, reset_path functions; new operations such as
@@ -88,6 +89,10 @@
 * added ML_PLATFORM setting (useful for cross-platform installations);
 more robust handling of platform specific ML images for SML/NJ;
 
+* the settings environment is now statically scoped, i.e. it is never
+read again in sub-processes invoked from isabelle, isatool, or
+Isabelle;
+
 * path element specification '~~' refers to '$ISABELLE_HOME';
 
 * in locales, the "assumes" and "defines" parts may be omitted if