refined Future.fork interfaces, no longer export Future.future;

fork/map: no inheritance of group (structure is nested, not parallel); removed group thread_data; refined Future.fork interfaces, no longer export Future.future;

future proofs: pass actual futures to facilitate composite computations; removed join_futures -- superceded by higher-level PureThy.force_proofs;

renamed type Lazy.T to lazy; force_proofs: original order;

future_scheduler: no global task group, exceptions via collective join; finish: removed PureThy.force_proofs, back to old version;

renamed type Lazy.T to lazy; renamed type Future.T to future;

excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;