summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 tip

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

merged