Re: [isabelle] Isabelle2015-RC3: Spurious "Duplicate rewrite rule" warnings during Sledgehammer invocation.
Small follow up,
when selecting a found proof Sledgehammer keeps running and during this
time the syntax highlighting is wrong (apply blue instead of red) and
the inserted command isn't processed until Sledgehammer finished
Am 08.05.15 um 10:59 schrieb bnord:
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