NEWS

--- a/NEWS	Wed Oct 13 15:16:52 1999 +0200
+++ b/NEWS	Wed Oct 13 15:18:15 1999 +0200
@@ -17,6 +17,9 @@
 
 * HOL: the predicate "inj" is now defined by translation to "inj_on";
 
+* HOL/datatype: mutual_induct_tac no longer exists --
+  use induct_tac "x_1 ... x_n" instead of mutual_induct_tac ["x_1", ..., "x_n"]
+
 * HOL/typedef: fixed type inference for representing set; type
 arguments now have to occur explicitly on the rhs as type constraints;