# HG changeset patch
# User wenzelm
# Date 978553288 -3600
# Node ID 4858ad0b8f3888eb391ce0be5ef6c79ef0ba5fe9
# Parent  70b9b0cfe05ff5a563f5d94260432a6588e80b2b
* Isar/HOL: added 'recdef_tc' command;

diff -r 70b9b0cfe05f -r 4858ad0b8f38 NEWS
--- 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 ***