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> 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.