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

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

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

moved generic instance to distribution

clarified signature: support partial read_proof to accommodate proof term normalization vs. approximative proof_boxes as upper bound;

turn hidden terms into dummy, e.g. relevant for boundary cases of reconstruct_proof;

support dummy term;

tuned signature;

proof boxes based on proof digest (not proof term): thus it works with prune_proofs;

proper Thm.transfer;

clarified files;

clarified proof_boxes (requires prune_proofs=false);

tuned;