Add a command "why3 play"
That command would take a list of mlw files and try to prove them with the specified provers and strategies, saving them to a session. It should also be able to play sessions by clearing the proof attempts (?), and try to prove all proof nodes again. At the end it should display a short report saying how many proof attempts were successful.