Allow running provers in parallel during strategy execution
This MR adds a new syntax to the call
step of strategies allowing you to use |
to separate multiple provers which will be invoked in parallel.
If a prover finishes before the others in it's group, it will interrupt them, potentially reducing the execution time of long strategies dramatically by avoiding sequential prover steps.
It does not change the default strategies (yet), though I could do that with not much effort.