Peter Lammich

2016-08-31 15:11:30 UTC

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

"$AFP/Refine_Monadic/Refine_Monadic"

begin

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

--

Peter

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

"$AFP/Refine_Monadic/Refine_Monadic"

begin

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

--

Peter