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 [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
