summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | berghofe |

Thu, 07 Oct 1999 12:52:23 +0200 | |

changeset 7780 | 099742c562aa |

parent 7779 | c80fc06972df |

child 7781 | 7a8e91b8c100 |

Documented changes to HOL/inductive and function thm_deps.

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