tuned;

proper p' instead of p (amending 52c7c42e7e27);

proper context for Goal.prove_internal;

discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily; Simplifier and equational conversions demand a proper proof context;

more accurate treatment of context, notably for nested Goal.proof / SUBPROOF;

tuned;

tuned;

tuned;

spelling;

clarified context;