Re: [isabelle] yet another simplifier question



Sledgehammer is a very complicated subsystem of Isabelle, which attempts to prove subgoals using external provers. It is often successful, but of course, many problems are too difficult for it.

Your first problem looks like it would be quite easy if you call the simplifier using divide_simps (and donât forget to include your assumption a>0).

And yes, you definitely need to use a recent version of Isabelle. I suggest that you download the release candidate,

http://isabelle.in.tum.de/website-Isabelle2016-1-RC2 <http://isabelle.in.tum.de/website-Isabelle2016-1-RC2>. 


Larry Paulson


> On 6 Nov 2016, at 17:16, noam neer <noamneer at gmail.com> wrote:
> 
> I just experimented with sledgehammer for the first time.
> it seems quite impressive, but also a little unstable.
> sometimes it doesn't return any output, sometimes I get messages like 
>     "z3": Timed out.
>     (and four more lines like this)
> and sometimes it does return a useful command.
> so it seems I always have to try it several times.
> is there a way to make it more stable?
> I'm using the default installation of Isabelle 2015 on win7.




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