NEWS
changeset 4388 c54f2e3423f2
parent 4381 99dfc9171f1e
child 4410 b68047c56fce
--- a/NEWS	Thu Dec 11 10:30:33 1997 +0100
+++ b/NEWS	Thu Dec 11 13:15:06 1997 +0100
@@ -48,7 +48,7 @@
 * print_goals: optional output of const types (set show_consts and
 show_types);
 
-* improved output of warnings (###) / errors (***);
+* improved output of warnings (###) and errors (***);
 
 * subgoal_tac displays a warning if the new subgoal has type variables;
 
@@ -61,8 +61,8 @@
 * deleted the obsolete tactical STATE, which was declared by
     fun STATE tacfun st = tacfun st st;
 
-* cd, use, use etc. now support path variables, e.g. ~ (which
-abbreviates $HOME), or $ISABELLE_HOME;
+* cd and use now support path variables, e.g. $ISABELLE_HOME, or ~
+(which abbreviates $HOME);
 
 * changed Pure/Sequence interface (see Pure/seq.ML); COMPATIBILITY:
 use isatool fixseq to adapt your ML programs (this works for fully