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?
> 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
> How can I apply sledgehammer to solve all subgoals?
> lemma "True & True"
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and