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