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).

Gerwin

> 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.
> 
> Tobias
> 
> 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.
>> 
>> Cheers,
>> Gerwin
>> 
>> 
>> ________________________________
>> 
>> 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 MHonArc.