[prove] give more information on failure
Sometimes giving the name and "expl" (eg "[postcondition]") of an invalid (sub)goal is sufficient to spot the problem. Printing them in the report would help avoiding to open the IDE
Sometimes giving the name and "expl" (eg "[postcondition]") of an invalid (sub)goal is sufficient to spot the problem. Printing them in the report would help avoiding to open the IDE