Quoting Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:
> Our current policy is the Plain, Main and Complex_Main are either > ancestors or descendants of any theory. OK, the requirement for Plain I can understand. For Main, it doesn't seem too unreasonable, assuming it's necessary (since most theory files import Main anyway). But Complex_Main? Are you serious? Implementing this policy would require changes to a LOT of theories: HOLCF, every subdirectory of src/HOL, all the AFP contributions, all user-created Isabelle theories in the entire world that import Main, etc. - Brian
