* Theory loader: old-style ML proof scripts are considered a legacy feature;
authorwenzelm
Wed Aug 08 23:07:46 2007 +0200 (2007-08-08)
changeset 241878bdf5ca5871f
parent 24186 d7f267b806c9
child 24188 d5960310c4d5
* Theory loader: old-style ML proof scripts are considered a legacy feature;
NEWS
     1.1 --- a/NEWS	Wed Aug 08 20:48:08 2007 +0200
     1.2 +++ b/NEWS	Wed Aug 08 23:07:46 2007 +0200
     1.3 @@ -41,6 +41,11 @@
     1.4  non-finished theories in persistent session images, such that source
     1.5  files may be moved later on without requiring reloads.
     1.6  
     1.7 +* Theory loader: old-style ML proof scripts being *attached* to a thy
     1.8 +file (with the same base name as the theory) are considered a legacy
     1.9 +feature, which will disappear eventually. Even now, the theory loader no
    1.10 +longer maintains dependencies on such files.
    1.11 +
    1.12  * Legacy goal package: reduced interface to the bare minimum required
    1.13  to keep existing proof scripts running.  Most other user-level
    1.14  functions are now part of the OldGoals structure, which is *not* open