clarified types (again): 'a is canonical for 'class' (as alternative to 'locale'), 'b is common for Hindley-Milner examples;

export constdefs according to defs.ML;

avoid spurious shyps (with vacous type variable);

merged

more robust hybrid treatment of Pure, notably for Isabelle/Dedukti;

clarified signature: name of standard_proof is authentic, otherwise empty;

clarified expand_proof/expand_name: allow more detailed control via thm_header; export_standard_proofs: authentic theorem names in "print" format;

option to export standardized proof terms (not scalable);

more kinds, notably for Isabelle/MMT;

refined proof of concept for bit operations

more lemmas

merged

export toplevel proof similar to named PThm;

tuned signature;

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;

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);