Re: [isabelle] Isabelle2015-RC3: Spurious "Duplicate rewrite rule" warnings during Sledgehammer invocation.
I observed the following confusing behaviour while porting part of my
development from I14 to I15RC3:
I had some broken mentis calls in some "don't care proofs" so I simply
invoked Sledgehammer there. While Sledgehammer was running the "apply
auto" or "using" right in front of it suddenly was underlined orange and
a couple of "ignoring duplicate rewrite rule" warnings (listing local
facts) popped up in the output. After Sledgehammer finished running the
warning disappeared again.
Another small focus problem which I find confusing: When the
Sledgehammer panel isn't in focus you can mouse over a suggested proof
and it will be highlighted but when you click on it nothing happens
besides switching focus.
This archive was generated by a fusion of
Pipermail (Mailman edition) and