[isabelle-dev] "The following files are required to resolve theory imports"
makarius at sketis.net
Tue Aug 25 21:50:51 CEST 2015
On Wed, 19 Aug 2015, Makarius wrote:
> On Wed, 19 Aug 2015, Larry Paulson wrote:
>> I frequently look at finished theories when looking for useful theorems.
>> But I’ve noticed a new and undesirable behaviour: I get the message "The
>> following files are required to resolve theory imports” even though the
>> theory is finished, and presumably has already been imported. Dismiss the
>> message, and it re-appears at least once more.
> This is part of ongoing reforms about management of ML source files -- the
> option is called jedit_auto_resolve, and in d94f3afd69b6 I've just changed
> the default to give more time to rethink it.
It is back in Isabelle/46df28442a80: already loaded theories are
More information about the isabelle-dev