summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

NEWS

changeset 12608 | 2df381faa787 |

parent 12597 | 14822e4436bf |

child 12622 | 7592926925d4 |

--- a/NEWS Sat Dec 29 13:14:11 2001 +0100 +++ b/NEWS Sat Dec 29 18:34:42 2001 +0100 @@ -143,7 +143,7 @@ * HOL: properly declared induction rules less_induct and wf_induct_rule; -* HOLCF: domain package adapted to new-style theories, e.g. see +* HOLCF: domain package adapted to new-style theory format, e.g. see HOLCF/ex/Dnat.thy; * ZF: proper integration of logic-specific tools and packages, @@ -245,9 +245,9 @@ * HOL/GroupTheory: group theory examples including Sylow's theorem (by Florian Kammüller); -* HOL/IMP: updated and converted to new-style theory; several parts -turned into readable document, with proper Isar proof texts and some -explanations (by Gerwin Klein); +* HOL/IMP: updated and converted to new-style theory format; several +parts turned into readable document, with proper Isar proof texts and +some explanations (by Gerwin Klein); *** HOLCF *** @@ -267,8 +267,11 @@ * ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a typeless version of the formalism; +* ZF/IMP: updated and converted to new-style theory format; + * ZF/Induct: new directory for examples of inductive definitions, -including theory Multiset for multiset orderings; +including theory Multiset for multiset orderings; converted to +new-style theory format; * ZF: the integer library now covers quotients and remainders, with many laws relating division to addition, multiplication, etc.;