--- a/NEWS Fri Apr 10 13:40:29 1998 +0200
+++ b/NEWS Fri Apr 10 13:41:04 1998 +0200
@@ -20,6 +20,8 @@
delWrapper, delSWrapper: claset * string -> claset
getWrapper is renamed to appWrappers, getSWrapper to appSWrappers;
+* Inductive definitions now handle disjunctive premises correctly (HOL and ZF)
+
*** HOL ***
@@ -37,6 +39,12 @@
* HOL/Relation: renamed the relational operatotr r^-1 "converse" instead of
"inverse"
+* HOL/equalities: added many new laws involving unions, intersectinos,
+ difference, etc.
+
+* recdef can now declare non-recursive functions, with {} supplied as the
+ well-founded relation
+
* Simplifier:
-The rule expand_if is now part of the default simpset. This means that
@@ -62,7 +70,6 @@
* many new identities for unions, intersections, etc.;
-
New in Isabelle98 (January 1998)
--------------------------------