summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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