1.1 --- a/NEWS	Thu Feb 01 18:47:31 2001 +0100
     1.2 +++ b/NEWS	Thu Feb 01 20:42:34 2001 +0100
     1.3 @@ -84,6 +84,8 @@
     1.4  
     1.5  * Pure: predict failure of "show" in interactive mode;
     1.6  
     1.7 +* Pure: 'thms_containing' now takes actual terms as arguments;
     1.8 +
     1.9  * HOL: improved method 'induct' --- now handles non-atomic goals
    1.10  (potential INCOMPATIBILITY); tuned error handling;
    1.11  
    1.12 @@ -97,6 +99,8 @@
    1.13  
    1.14  * HOL: added 'recdef_tc' command;
    1.15  
    1.16 +* isatool convert assists in eliminating legacy ML scripts;
    1.17 +
    1.18  
    1.19  *** HOL ***
    1.20