--- 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