NEWS
changeset 7791 66d3b64dbf49
parent 7780 099742c562aa
child 7805 0ae9ddc36fe0
     1.1 --- a/NEWS	Thu Oct 07 22:36:52 1999 +0200
     1.2 +++ b/NEWS	Fri Oct 08 11:10:07 1999 +0200
     1.3 @@ -63,6 +63,9 @@
     1.4  Isabelle/Isar (the latter is slightly better supported and more
     1.5  robust);
     1.6  
     1.7 +* ML function thm_deps visualizes dependencies of theorems and lemmas,
     1.8 +using the graph browser tool;
     1.9 +
    1.10  * Isabelle manuals now also available as PDF;
    1.11  
    1.12  * improved browser info generation: better HTML markup (including
    1.13 @@ -116,9 +119,6 @@
    1.14  result is not stored, but proper checks and presentation of the result
    1.15  still apply;
    1.16  
    1.17 -* New function thm_deps for visualizing dependencies between theorems
    1.18 -  (using graph browser).
    1.19 -
    1.20  
    1.21  *** HOL ***
    1.22  
    1.23 @@ -181,13 +181,10 @@
    1.24  temporal levels more uniformly; introduces INCOMPATIBILITIES due to
    1.25  changed syntax and (many) tactics;
    1.26  
    1.27 -* HOL/inductive: Now also handles more complicated introduction rules
    1.28 -  such as
    1.29 -
    1.30 -  "ALL y. (y, x) : r --> y : acc r ==> x : acc r"
    1.31 -
    1.32 -  New monotonicity theorems can be added to a theory using the "mono"
    1.33 -  attribute.
    1.34 +* HOL/inductive: Now also handles more general introduction rules such
    1.35 +  as "ALL y. (y, x) : r --> y : acc r ==> x : acc r"; monotonicity
    1.36 +  theorems are now maintained within the theory (maintained via the
    1.37 +  "mono" attribute);
    1.38  
    1.39  * HOL/datatype: Now also handles arbitrarily branching datatypes
    1.40    (using function types) such as