tuned;
authorwenzelm
Thu, 11 Dec 1997 13:15:06 +0100
changeset 4388c54f2e3423f2
parent 4387 31d5a5a191e8
child 4389 1865cb8df116
tuned;
NEWS
     1.1 --- a/NEWS	Thu Dec 11 10:30:33 1997 +0100
     1.2 +++ b/NEWS	Thu Dec 11 13:15:06 1997 +0100
     1.3 @@ -48,7 +48,7 @@
     1.4  * print_goals: optional output of const types (set show_consts and
     1.5  show_types);
     1.6  
     1.7 -* improved output of warnings (###) / errors (***);
     1.8 +* improved output of warnings (###) and errors (***);
     1.9  
    1.10  * subgoal_tac displays a warning if the new subgoal has type variables;
    1.11  
    1.12 @@ -61,8 +61,8 @@
    1.13  * deleted the obsolete tactical STATE, which was declared by
    1.14      fun STATE tacfun st = tacfun st st;
    1.15  
    1.16 -* cd, use, use etc. now support path variables, e.g. ~ (which
    1.17 -abbreviates $HOME), or $ISABELLE_HOME;
    1.18 +* cd and use now support path variables, e.g. $ISABELLE_HOME, or ~
    1.19 +(which abbreviates $HOME);
    1.20  
    1.21  * changed Pure/Sequence interface (see Pure/seq.ML); COMPATIBILITY:
    1.22  use isatool fixseq to adapt your ML programs (this works for fully