Documented changes to HOL/inductive and function thm_deps.
authorberghofe
Thu Oct 07 12:52:23 1999 +0200 (1999-10-07)
changeset 7780099742c562aa
parent 7779 c80fc06972df
child 7781 7a8e91b8c100
Documented changes to HOL/inductive and function thm_deps.
NEWS
     1.1 --- a/NEWS	Thu Oct 07 12:51:37 1999 +0200
     1.2 +++ b/NEWS	Thu Oct 07 12:52:23 1999 +0200
     1.3 @@ -116,6 +116,9 @@
     1.4  result is not stored, but proper checks and presentation of the result
     1.5  still apply;
     1.6  
     1.7 +* New function thm_deps for visualizing dependencies between theorems
     1.8 +  (using graph browser).
     1.9 +
    1.10  
    1.11  *** HOL ***
    1.12  
    1.13 @@ -178,6 +181,14 @@
    1.14  temporal levels more uniformly; introduces INCOMPATIBILITIES due to
    1.15  changed syntax and (many) tactics;
    1.16  
    1.17 +* HOL/inductive: Now also handles more complicated introduction rules
    1.18 +  such as
    1.19 +
    1.20 +  "ALL y. (y, x) : r --> y : acc r ==> x : acc r"
    1.21 +
    1.22 +  New monotonicity theorems can be added to a theory using the "mono"
    1.23 +  attribute.
    1.24 +
    1.25  * HOL/datatype: Now also handles arbitrarily branching datatypes
    1.26    (using function types) such as
    1.27