[isabelle-dev] Typerep again
brianh at cs.pdx.edu
Tue Feb 10 00:27:09 CET 2009
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.
More information about the isabelle-dev