[isabelle-dev] Typerep again
ac638 at cam.ac.uk
Mon Feb 9 16:18:30 CET 2009
> and the fishing rules...
>>> Our current policy is that Plain, Main and Complex_Main are either
>>> ancestors or descendants of any theory.
> But feel free to ask if this is still obscure.
This rule does not tell me anything since it is trivally satisfied by
any connected graph containing Plain, Main and Complex_Main.
Do you mean that in the imports section of any theory one of the words
Plain, Main or complex Main should appear?
Can you give a precise description of what happens and how we should
circumvent these problems. I completely disagree with a rule that
obliges to import from a higher theory than necessary. This is just not
natural. If this mechanism is so important in HOL then it should be
either clarified to the developers and users or it should be done in a
manner not be noticed in a negative way.
More information about the isabelle-dev