Documented changes to HOL/inductive and function thm_deps.

--- a/NEWS	Thu Oct 07 12:51:37 1999 +0200
+++ b/NEWS	Thu Oct 07 12:52:23 1999 +0200
@@ -116,6 +116,9 @@
 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 ***
 
@@ -178,6 +181,14 @@
 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/datatype: Now also handles arbitrarily branching datatypes
   (using function types) such as