Re: [isabelle] simp warnings for cong rules

I agree. That is not something to warn about.

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