news.

--- a/NEWS	Fri May 23 14:13:51 1997 +0200
+++ b/NEWS	Fri May 23 14:17:40 1997 +0200
@@ -94,6 +94,11 @@
 * a generic induction tactic `induct_tac' which works for all datatypes and
 also for type `nat';
 
+* a generic case distinction tactic `exhaust_tac' which works for all
+datatypes and also for type `nat';
+
+* each datatype comes with a function `size';
+
 * patterns in case expressions allow tuple patterns as arguments to
 constructors, for example `case x of [] => ... | (x,y,z)#ps => ...';