# HG changeset patch
# User paulson
# Date 917449794 -3600
# Node ID e387d188d0caf201b27e63323a0ee92c3ac6548c
# Parent  6a00a5baef2b19a3b414135e669538ad68c5d550
ZF typechecking

diff -r 6a00a5baef2b -r e387d188d0ca NEWS
--- 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).