--- a/NEWS Tue Jan 19 11:16:39 1999 +0100
+++ b/NEWS Tue Jan 19 11:18:11 1999 +0100
@@ -11,6 +11,10 @@
* ZF: The con_defs part of an inductive definition may no longer refer to
constants declared in the same theory;
+* HOL, ZF: the function mk_cases, generated by the inductive definition
+ package, has lost an argument. To simplify its result, it uses the default
+ simpset instead of a supplied list of theorems.
+
*** Proof tools ***
@@ -68,6 +72,9 @@
* the datatype declaration of type T now defines the recursor T_rec;
+* simplification automatically does freeness reasoning for datatype
+ constructors;
+
* The syntax "if P then x else y" is now available in addition to if(P,x,y).