* Pure: 'thms_containing' now takes actual terms as arguments;
* isatool convert assists in eliminating legacy ML scripts;

--- 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 ***