Re: [isabelle] Sledgehammer all subgoals?



> On 15 Sep 2015, at 11:05, Tom Ridge <tom.j.ridge at googlemail.com> wrote:
> 
> If it is not too much effort to add, this feature would be quite useful to me (and to others?). Presumably the implementation is easy - conjunct-up the goals and feed them to sledgehammer?

This particular suggestion would not work. You would get nothing unless all the goals could be solved, and forming the conjunction of two problems is particularly damaging for resolution (to see why, consider the details of the translation into clause form).

Canât you identify the difficult case simply by looking at it? And possibly the simp_all method could be of use here.

Larry Paulson






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