Failed POs are now removed from the Isabelle buffer so that additional lemmas can be proved afterwards