back to polyml-5.4.1 (cf. b3110dec1a32) -- no cause of spurious interrupts;

merged

back to parallel HOL-BNF-Examples, which seems to have suffered from Future.map on canceled persistent futures;

more basic Goal.reset_futures as snapshot of implicit state;
more robust Session.finish_futures: do not cancel here, to allow later Future.map of persistent futures (notably proof terms);

tuned proof;

update RBT_Mapping, AList_Mapping and Mapping to use lifting/transfer

tuned proofs

new theorem

merged

merged