[isabelle] sledgehammer issue

Hi Jasmin,

In Isabelle2016, I get the following weird sledgehammer output.

Sometimes, (I could not reproduce with small example), I also get the
message that e derived false from these facts, and that I should report
this as a "bug" in sledgehammer.

theory Scratch
imports MainÂ

 lemma "A=B"
ÂÂÂÂusing ASSERT_simps(1) inres_simps(3) pw_ASSERT(2)
ÂÂÂÂsledgehammer [provers = e]
(* Sledgehammering...Â
"e": Try this: by metis (> 1.0 s, timed out).
 oops  Â


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.