# HG changeset patch
# User wenzelm
# Date 881507395 -3600
# Node ID 99dfc9171f1eaf99eb9e2086e70c259d24138bb5
# Parent  0a32020760fa2830257837849d0e3fe50dfa4d22
tuned;

diff -r 0a32020760fa -r 99dfc9171f1e NEWS
--- a/NEWS	Sun Dec 07 16:05:36 1997 +0100
+++ b/NEWS	Sun Dec 07 16:09:55 1997 +0100
@@ -68,7 +68,8 @@
 use isatool fixseq to adapt your ML programs (this works for fully
 qualified references to the Sequence structure only!);
 
-* use_thy no longer requires writable current directory;
+* use_thy no longer requires writable current directory; it always
+reloads .ML *and* .thy file, if either one is out of date;
 
 
 *** Classical Reasoner ***