1.1 --- a/NEWS	Fri Apr 10 13:40:29 1998 +0200
     1.2 +++ b/NEWS	Fri Apr 10 13:41:04 1998 +0200
     1.3 @@ -20,6 +20,8 @@
     1.4    delWrapper, delSWrapper: claset *  string -> claset
     1.5    getWrapper is renamed to appWrappers, getSWrapper to appSWrappers;
     1.6  
     1.7 +* Inductive definitions now handle disjunctive premises correctly (HOL and ZF)
     1.8 +
     1.9  
    1.10  *** HOL ***
    1.11  
    1.12 @@ -37,6 +39,12 @@
    1.13  * HOL/Relation: renamed the relational operatotr r^-1 "converse" instead of
    1.14    "inverse"
    1.15  
    1.16 +* HOL/equalities: added many new laws involving unions, intersectinos,
    1.17 +  difference, etc.
    1.18 +
    1.19 +* recdef can now declare non-recursive functions, with {} supplied as the 
    1.20 +  well-founded relation
    1.21 +
    1.22  * Simplifier:
    1.23  
    1.24   -The rule expand_if is now part of the default simpset. This means that
    1.25 @@ -62,7 +70,6 @@
    1.26  * many new identities for unions, intersections, etc.;
    1.27  
    1.28  
    1.29 -
    1.30  New in Isabelle98 (January 1998)
    1.31  --------------------------------
    1.32