ZF typechecking

--- a/NEWS	Wed Jan 27 15:58:22 1999 +0100
+++ b/NEWS	Wed Jan 27 16:09:54 1999 +0100
@@ -75,6 +75,12 @@
 * simplification automatically does freeness reasoning for datatype
   constructors;
 
+* automatic type-inference, with AddTCs command to insert new type-checking
+  rules;
+
+* datatype introduction rules are now added as Safe Introduction rules to
+  the claset;
+
 * The syntax "if P then x else y" is now available in addition to if(P,x,y).