# 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 ***