* Theory loader: old-style ML proof scripts being *attached* to a thy file are no longer supported. INCOMPATIBILITY, regular 'uses' and 'use' within a theory file will do the job.