[isabelle] Sledgehammer all subgoals?



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.