Re: [isabelle] Isabelle-RCX/Windows 64 bits (Sledgehammer)

On Fri, 29 Jan 2016, Alfio Martini wrote:

In Isabelle-RC2 and -RC1, Sledgehammer often fails to find a proof for the
notorious lemma about indexed sums (with
or without try methods):

lemma aux: "m <= n+1 ==> setsum f {m..n + 1} =
   setsum f {m..n} + f (n + 1 :: int)"

OS: Windows 10 with a Intel i5-5200U CPU @ 2.20GHz

I've briefly tried this with with Isabelle2015 and Isabelle2016-RC3 on Linux, and it fails consistently for all provers.

It is unclear to me if one could expect this to work. It depends a lot on HOL library contents, and these change frequently.


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