[isabelle] Sledgehammer option to stop if first prover finds a proof



Hi,

is there an option that stops the other provers if sledgehammer finds a
proof.

Use-case:
  I have several subgoals, and want to see which of them are (easily)
provable. So, currently, I invoke sledgehammer in parallel on all
subgoals:

  subgoal sledgehammer sorry
  subgoal sledgehammer sorry
  ...
  subgoal sledgehammer sorry
		

In order to make this effeicient, the sledgehammer tool should stop if
it has found and reconstructed SOME proof, to give its resources to the
remaining sledgehammers.

Of course, a sledgehammer-all-subgoals command would be even better.

Best,
  Peter





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