[isabelle-dev] "The following files are required to resolve theory imports"
lp15 at cam.ac.uk
Wed Aug 19 12:55:15 CEST 2015
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.
More information about the isabelle-dev