NEWS
changeset 24187 8bdf5ca5871f
parent 24172 06e42cf7df4e
child 24210 a865059c4fcb
     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