--- a/NEWS Fri Jan 19 23:53:07 2001 +0100
+++ b/NEWS Sat Jan 20 00:01:40 2001 +0100
@@ -1,3 +1,4 @@
+
Isabelle NEWS -- history user-relevant changes
==============================================
@@ -77,6 +78,8 @@
* Pure: 'thm_deps' command visualizes dependencies of theorems and
lemmas, using the graph browser tool;
+* Pure: predict failure of "show" in interactive mode;
+
* HOL: improved method 'induct' --- now handles non-atomic goals
(potential INCOMPATIBILITY); tuned error handling;
@@ -116,8 +119,8 @@
* HOL: improved concrete syntax for strings (e.g. allows translation
rules with string literals);
-* HOL-Hyperreal: a new target, extending HOL-Real with the hyperreals and
-Fleuriot's mechanization of analysis;
+* HOL-Hyperreal: a new target, extending HOL-Real with the hyperreals
+and Fleuriot's mechanization of analysis;
* HOL-Real, HOL-Hyperreals: improved arithmetic simplification;