1.1 --- a/NEWS	Tue Nov 13 22:24:28 2001 +0100
     1.2 +++ b/NEWS	Tue Nov 13 22:25:59 2001 +0100
     1.3 @@ -209,14 +209,17 @@
     1.4  
     1.5  *** ZF ***
     1.6  
     1.7 +* ZF: new-style theory commands 'inductive', 'inductive_cases', and
     1.8 +methods 'ind_cases', 'induct_tac', 'case_tac';
     1.9 +
    1.10  * ZF: the integer library now covers quotients and remainders, with
    1.11  many laws relating division to addition, multiplication, etc.;
    1.12  
    1.13 -* ZF/Induct: new directory for examples of inductive definitions, including theory
    1.14 -Multiset for multiset orderings;
    1.15 -
    1.16 -* ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a typeless
    1.17 -version of the formalism;
    1.18 +* ZF/Induct: new directory for examples of inductive definitions,
    1.19 +including theory Multiset for multiset orderings;
    1.20 +
    1.21 +* ZF/UNITY: Chandy and Misra's UNITY is now available in ZF, giving a
    1.22 +typeless version of the formalism;
    1.23  
    1.24  
    1.25  *** General ***