Re: [isabelle] Sledgehammer all subgoals?



I don't believe that such an option exists. Even with one goal, you are spawning up to 5 subprocesses on your machine. The idea anyway that you are trying to tackle a particularly tough problem, so it's natural to tackle them one at a time.

I wonder: is there much demand for this option?

Larry

> On 15 Sep 2015, at 09:14, Tom Ridge via Cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk> wrote:
> 
> Dear All,
> 
> Sorry for the easy question, but I couldn't find the answer in the
> documentation.
> 
> How can I apply sledgehammer to solve all subgoals?
> 
> e.g.
> 
> lemma "True & True"
> apply(rule)
> 
> At this point, if I click on the "Sledgehammer" tab in jedit and click
> apply, it shows me a solution to the first goal. But I want it to solve all
> the goals.
> 
> Thanks





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