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

proper protocol_message for bootstrap proofs;

proper export of bootstrap proofs (amending a6304b4664b6);

more robust -- avoid interference with Proofterm.proofs := 0 in ML_Bootstrap.thy;

proper treatment of self thm_id;
clarified signature;

added quickcheck setup

generalized

moved quickcheck setup to distribution

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;