Proof.future_proof: declare all assumptions as well; Proof.future_proof: removed spurious exception_trace (which might cause crash-by-interrupt); replaced Future.fork_local by Future.fork_pri (again, until group exceptions are propagated properly);

parallel_proofs: more fine-grained control with optional parallel checking of nested Isar proofs;

cancel_proofs: some attempts at reworking group management (based on body promises only);

support for arbitrarity nested future proofs -- replaced crude order by explicit normalization (which might loop for bad dependencies); export promises_of; removed obsolete pending_groups; tuned;