author | berghofe |

Thu Oct 07 12:52:23 1999 +0200 (1999-10-07) | |

changeset 7780 | 099742c562aa |

parent 7779 | c80fc06972df |

child 7781 | 7a8e91b8c100 |

Documented changes to HOL/inductive and function thm_deps.

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