Re: [isabelle] Difficulties with "setsum" (Alfio Martini)
On Wed, 22 Apr 2015, Alfio Martini wrote:
I use the Windows installation of Isabelle 2014 and my sledgehammer
installation does not find any proof for this lemma. Actually, it never
finds any proof whatsoever. I have just realized that it does not solve
even that lemma in section 3 (First Steps) of the Sledgehammer tutorial. I
have always used Sledgehammer as it is packaged. I just set z3
use to "yes". The prover "remote-vampire" is never available (literally),
while e, spass and z3 always time out.
I will have to take a look into this. This is really making may Isabelle
experience miserable at the moment.
There is Isabelle2015-RC1 already, to try if the situation has improved.
If not, we also need a bit of information about your hardware and
operating system version.
I am not aware of any such problems in Isabelle2014 or Isabelle2015-RC1,
so unless there are tangible problem reports, the problems don't exist.
This archive was generated by a fusion of
Pipermail (Mailman edition) and