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

Reply via email to