register proofs of Isar goals, to enable recovery from unstable command states after interactive cancellation;

refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390); stretched meaning of Goal.parallel_proofs to enable future_terminal_proofs in interactive document model, despite its lack for regular forking of proofs;

some support for registering forked proofs within Proof.state, using its bottom context; tuned signature;

tuned signature;

refined status of forked goals;

proper merge of promises to avoid exponential blow-up in pathologic situations (e.g. lack of PThm wrapping);

tuned message;