[isabelle-dev] "The following files are required to resolve theory imports"

[Larry Paulson]

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.

Larry