# HG changeset patch
# User wenzelm
# Date 981056554 -3600
# Node ID 8f8ba41a5e7ae4b065ff6b680578bc389d0e5c8f
# Parent  55d95834c815763734b4e3ed10c9d017cb11c1ff
* Pure: 'thms_containing' now takes actual terms as arguments;
* isatool convert assists in eliminating legacy ML scripts;

diff -r 55d95834c815 -r 8f8ba41a5e7a NEWS
--- a/NEWS	Thu Feb 01 18:47:31 2001 +0100
+++ b/NEWS	Thu Feb 01 20:42:34 2001 +0100
@@ -84,6 +84,8 @@
 
 * Pure: predict failure of "show" in interactive mode;
 
+* Pure: 'thms_containing' now takes actual terms as arguments;
+
 * HOL: improved method 'induct' --- now handles non-atomic goals
 (potential INCOMPATIBILITY); tuned error handling;
 
@@ -97,6 +99,8 @@
 
 * HOL: added 'recdef_tc' command;
 
+* isatool convert assists in eliminating legacy ML scripts;
+
 
 *** HOL ***