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