[isabelle-dev] Typerep again

[Brian Huffman]

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