NEWS
changeset 10944 710ddb9e8b5e
parent 10915 6b66a8a530ce
child 10966 8f2c27041a8e
     1.1 --- a/NEWS	Fri Jan 19 23:53:07 2001 +0100
     1.2 +++ b/NEWS	Sat Jan 20 00:01:40 2001 +0100
     1.3 @@ -1,3 +1,4 @@
     1.4 +
     1.5  Isabelle NEWS -- history user-relevant changes
     1.6  ==============================================
     1.7  
     1.8 @@ -77,6 +78,8 @@
     1.9  * Pure: 'thm_deps' command visualizes dependencies of theorems and
    1.10  lemmas, using the graph browser tool;
    1.11  
    1.12 +* Pure: predict failure of "show" in interactive mode;
    1.13 +
    1.14  * HOL: improved method 'induct' --- now handles non-atomic goals
    1.15  (potential INCOMPATIBILITY); tuned error handling;
    1.16  
    1.17 @@ -116,8 +119,8 @@
    1.18  * HOL: improved concrete syntax for strings (e.g. allows translation
    1.19  rules with string literals);
    1.20  
    1.21 -* HOL-Hyperreal: a new target, extending HOL-Real with the hyperreals and 
    1.22 -Fleuriot's mechanization of analysis;
    1.23 +* HOL-Hyperreal: a new target, extending HOL-Real with the hyperreals
    1.24 +and Fleuriot's mechanization of analysis;
    1.25  
    1.26  * HOL-Real, HOL-Hyperreals: improved arithmetic simplification;
    1.27