wenzelm [Sat, 13 Oct 2012 18:04:11 +0200] rev 49846
refined Proof.the_finished_goal with more informative error;
more permissive Method.all_assm_tac: do not insist in solving by assumption here to postpone failure;
clarified Method.finish_text: no Thm.no_prems filtering here to postpone failure;