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

Tjark Weber webertj at in.tum.de
Fri Jan 21 15:23:27 CET 2011


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,

More information about the isabelle-dev mailing list