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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
