--- a/NEWS Wed Jan 03 21:20:40 2001 +0100
+++ b/NEWS Wed Jan 03 21:21:28 2001 +0100
@@ -62,6 +62,8 @@
number of facts to be consumed (0 for "type" and 1 for "set" rules);
any remaining facts are inserted into the goal verbatim;
+* HOL: added 'recdef_tc' command;
+
*** HOL ***