* ZF/IMP: updated and converted to new-style theory format;
authorwenzelm
Sat Dec 29 18:34:42 2001 +0100 (2001-12-29)
changeset 126082df381faa787
parent 12607 16b63730cfbb
child 12609 fb073a34b537
* ZF/IMP: updated and converted to new-style theory format;
NEWS
     1.1 --- a/NEWS	Sat Dec 29 13:14:11 2001 +0100
     1.2 +++ b/NEWS	Sat Dec 29 18:34:42 2001 +0100
     1.3 @@ -143,7 +143,7 @@
     1.4  * HOL: properly declared induction rules less_induct and
     1.5  wf_induct_rule;
     1.6  
     1.7 -* HOLCF: domain package adapted to new-style theories, e.g. see
     1.8 +* HOLCF: domain package adapted to new-style theory format, e.g. see
     1.9  HOLCF/ex/Dnat.thy;
    1.10  
    1.11  * ZF: proper integration of logic-specific tools and packages,
    1.12 @@ -245,9 +245,9 @@
    1.13  * HOL/GroupTheory: group theory examples including Sylow's theorem (by
    1.14  Florian Kammüller);
    1.15  
    1.16 -* HOL/IMP: updated and converted to new-style theory; several parts
    1.17 -turned into readable document, with proper Isar proof texts and some
    1.18 -explanations (by Gerwin Klein);
    1.19 +* HOL/IMP: updated and converted to new-style theory format; several
    1.20 +parts turned into readable document, with proper Isar proof texts and
    1.21 +some explanations (by Gerwin Klein);
    1.22  
    1.23  
    1.24  *** HOLCF ***
    1.25 @@ -267,8 +267,11 @@
    1.26  * ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a
    1.27  typeless version of the formalism;
    1.28  
    1.29 +* ZF/IMP: updated and converted to new-style theory format;
    1.30 +
    1.31  * ZF/Induct: new directory for examples of inductive definitions,
    1.32 -including theory Multiset for multiset orderings;
    1.33 +including theory Multiset for multiset orderings; converted to
    1.34 +new-style theory format;
    1.35  
    1.36  * ZF: the integer library now covers quotients and remainders, with
    1.37  many laws relating division to addition, multiplication, etc.;