Re: [isabelle] simp warnings for cong rules



I agree. That is not something to warn about.
Larry

> On 11 May 2015, at 09:26, Gerwin Klein <gerwin.klein at nicta.com.au> 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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.