#1038 (Oct 21, 2019, 12:50:07 AM)

1. avoid spurious shyps (with vacous type variable); (detail / hgweb)
2. merged (detail / hgweb)
3. more robust hybrid treatment of Pure, notably for Isabelle/Dedukti; (detail / hgweb)
4. clarified signature: name of standard_proof is authentic, otherwise empty; (detail / hgweb)
5. clarified expand_proof/expand_name: allow more detailed control via thm_header;
   export_standard_proofs: authentic theorem names in "print" format; (detail / hgweb)
6. option to export standardized proof terms (not scalable); (detail / hgweb)
7. more kinds, notably for Isabelle/MMT; (detail / hgweb)
8. refined proof of concept for bit operations (detail / hgweb)
9. more lemmas (detail / hgweb)

Started by an SCM change

This run spent:

• 6.2 sec waiting;
• 1 hr 21 min build duration;
• 1 hr 21 min total from scheduled to completion.