tuned;
authorwenzelm
Tue May 18 15:52:34 1999 +0200 (1999-05-18)
changeset 6671677713791bd8
parent 6670 4921b1f8ff92
child 6672 8542c6dda828
tuned;
NEWS
     1.1 --- a/NEWS	Tue May 18 12:36:06 1999 +0200
     1.2 +++ b/NEWS	Tue May 18 15:52:34 1999 +0200
     1.3 @@ -33,9 +33,14 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* improved browser info generation: better HTML markup (including
     1.8 +colors), graph views in several sizes; isatool usedir now provides a
     1.9 +proper interface for user theories (via -P option);
    1.10 +
    1.11  * theory loader rewritten from scratch (may not be fully
    1.12  bug-compatible); old loadpath variable has been replaced by show_path,
    1.13 -add_path, del_path, reset_path functions;
    1.14 +add_path, del_path, reset_path functions; new operations such as
    1.15 +update_thy, touch_thy, remove_thy (see also isatool doc ref);
    1.16  
    1.17  * in locales, the "assumes" and "defines" parts may be omitted if
    1.18  empty;
    1.19 @@ -54,6 +59,7 @@
    1.20  option -p DIR installs standalone binaries;
    1.21  
    1.22  * added ML_PLATFORM setting (useful for cross-platform installations);
    1.23 +more robust handling of platform specific ML images for SML/NJ;
    1.24  
    1.25  * Isamode 2.6 requires patch to accomodate change of Isabelle font
    1.26  mode and goal output format:
    1.27 @@ -105,7 +111,8 @@
    1.28  * HOL/typedef: fixed type inference for representing set; type
    1.29  arguments now have to occur explicitly on the rhs as type constraints;
    1.30  
    1.31 -* HOL/recdef (TFL) now requires theory Recdef;
    1.32 +* HOL/recdef (TFL): requires theory Recdef; 'congs' syntax now expects
    1.33 +comma separated list of theorem names rather than an ML expression;
    1.34  
    1.35  
    1.36  *** ZF ***