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 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and