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

[Tobias Nipkow]

One issue can be that if some sort involves multiple type classes, the
corresponding class may not have been defined. That is the one advantage
of sorts: you can create conjunctions/intersection of type classes on
the fly.

Tobias

Tjark Weber schrieb:
> 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
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev