[isabelle-dev] Sort Annotation vs. Class Context for Lemmas

[Tjark Weber]

Hi,

I noticed that numerous lemmas in HOL that refer to class constants are
stated at the top level (using implicit or explicit sort annotations),
rather than in the corresponding class context (see, for instance,
Compl_lessThan in HOL/SetInterval.thy).  If I am not mistaken, this
means the corresponding lemma is not available in the context of the
class, which seems unfortunate.  Is this merely a legacy issue, or are
there genuine reasons for stating these lemmas with sort annotations?

Kind regards,
Tjark