[isabelle-dev] Typerep again

[Amine Chaieb]

 > 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.

Amine