Re: [isabelle] Isabelle2015-RC3: Spurious "Duplicate rewrite rule" warnings during Sledgehammer invocation.
On Fri, 8 May 2015, Lars Noschinski wrote:
These stray warnings had a nice little side-effect for me: They notified
me that sledgehammer had found a proof. As I often switch to the output
or query panels when sledgehammer is busy, this was often useful.
BTW: https://xkcd.com/1172/ ;)
This well-known cartoon proves that the words "bug" and "feature" are
A problem with the current situation is that we still have too many
"modes" of sledgehammer, some obsolete after the removal of TTY / Proof
Before the change bcd9a70342be, I did not know that the main entry point
of sledgehammer has moved elsewhere. There are more details like
treatment of "using" facts that are unified by it, not just disabling
Incremental results can be emitted indepently of that as official
information messages. I don't know why this was not tried before,
probably also because of too much "modes" confusion.
Presently on the release ramp, we should concentrate on the real problems,
such as robust Windows support.
This archive was generated by a fusion of
Pipermail (Mailman edition) and