# HG changeset patch
# User wenzelm
# Date 979945300 -3600
# Node ID 710ddb9e8b5e9868d7576459d8aa01d871c775e7
# Parent  3a610d34eb9e1f81a10363089252a09b530aded4
*** empty log message ***

diff -r 3a610d34eb9e -r 710ddb9e8b5e NEWS
--- 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;