changeset 4381 | 99dfc9171f1e |
parent 4373 | 2f831a45d571 |
child 4388 | c54f2e3423f2 |
--- 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 ***