Re: [isabelle] simp warnings for cong rules
I now realise what they were useful for originally: when you declare [cong] globally, to set up a library for instance, you want to be warned if a constant already has a cong rule. If you use them locally, you donât want to know about it.
Probably the same for intro!/intro
Would probably mean passing another parameter into the implementation to distinguish the global from the local use (unless you can already tell by something else).
> On 11 May 2015, at 2:11 pm, Tobias Nipkow <nipkow at in.tum.de> wrote:
> I am tempted to remove these altogether. I had done so alread with warnings about overwriting split rules.
> On 11/05/2015 10:26, Gerwin Klein wrote:
>> Overwriting congruence rule for âHOL.Ifâ
>> Should these really be warning messages or should we classify them as âtraceâ or something similar?
>> Warnings light up fairly prominently in jedit these days, and such messages distract for warnings that you want to do something about.
>> The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
This archive was generated by a fusion of
Pipermail (Mailman edition) and