clarified ML toplevel output: avoid "??." prefix;

tuned;

merged

use strict Global_Theory.register_proofs as checkpoint for stored zproof, and thus reduce current zboxes;

clarified signature;

omit pointless future: proof terms are built sequentially;

omit unclear / inaccurate renaming;

more normalization: re-use Thm.solve_constraints as important checkpoint for results, notably Global_Theory.name_thm;

more robust: avoid assumption about Context.certificate_theory;

tuned;