# HG changeset patch
# User wenzelm
# Date 939373807 -7200
# Node ID 66d3b64dbf49448279804845feb1f42bdaddda70
# Parent  2fd4d53acc0ac369692a64aa37d1d285a08cb93d
tuned;

diff -r 2fd4d53acc0a -r 66d3b64dbf49 NEWS
--- a/NEWS	Thu Oct 07 22:36:52 1999 +0200
+++ b/NEWS	Fri Oct 08 11:10:07 1999 +0200
@@ -63,6 +63,9 @@
 Isabelle/Isar (the latter is slightly better supported and more
 robust);
 
+* ML function thm_deps visualizes dependencies of theorems and lemmas,
+using the graph browser tool;
+
 * Isabelle manuals now also available as PDF;
 
 * improved browser info generation: better HTML markup (including
@@ -116,9 +119,6 @@
 result is not stored, but proper checks and presentation of the result
 still apply;
 
-* New function thm_deps for visualizing dependencies between theorems
-  (using graph browser).
-
 
 *** HOL ***
 
@@ -181,13 +181,10 @@
 temporal levels more uniformly; introduces INCOMPATIBILITIES due to
 changed syntax and (many) tactics;
 
-* HOL/inductive: Now also handles more complicated introduction rules
-  such as
-
-  "ALL y. (y, x) : r --> y : acc r ==> x : acc r"
-
-  New monotonicity theorems can be added to a theory using the "mono"
-  attribute.
+* HOL/inductive: Now also handles more general introduction rules such
+  as "ALL y. (y, x) : r --> y : acc r ==> x : acc r"; monotonicity
+  theorems are now maintained within the theory (maintained via the
+  "mono" attribute);
 
 * HOL/datatype: Now also handles arbitrarily branching datatypes
   (using function types) such as