* Pure: 'thms_containing' now takes actual terms as arguments;
authorwenzelm
Thu Feb 01 20:42:34 2001 +0100 (2001-02-01)
changeset 110168f8ba41a5e7a
parent 11015 55d95834c815
child 11017 241cbdf4134e
* Pure: 'thms_containing' now takes actual terms as arguments;
* isatool convert assists in eliminating legacy ML scripts;
NEWS
     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