# HG changeset patch
# User wenzelm
# Date 1186607266 -7200
# Node ID 8bdf5ca5871f522293af205ac6d932a87eaf4346
# Parent  d7f267b806c9659ac6628b1e01f6cf73f7318d5a
* Theory loader: old-style ML proof scripts are considered a legacy feature;

diff -r d7f267b806c9 -r 8bdf5ca5871f NEWS
--- a/NEWS	Wed Aug 08 20:48:08 2007 +0200
+++ b/NEWS	Wed Aug 08 23:07:46 2007 +0200
@@ -41,6 +41,11 @@
 non-finished theories in persistent session images, such that source
 files may be moved later on without requiring reloads.
 
+* Theory loader: old-style ML proof scripts being *attached* to a thy
+file (with the same base name as the theory) are considered a legacy
+feature, which will disappear eventually. Even now, the theory loader no
+longer maintains dependencies on such files.
+
 * Legacy goal package: reduced interface to the bare minimum required
 to keep existing proof scripts running.  Most other user-level
 functions are now part of the OldGoals structure, which is *not* open