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 MHonArc.