#1029 (Oct 12, 2019, 12:50:09 AM)

1. merged (detail / hgweb)
2. proper ML names; (detail / hgweb)
3. clarified standard_proof_of: prefer expand_proof over somewhat adhoc strip_thm_proof; (detail / hgweb)
4. some treatment of OfClass proofs; (detail / hgweb)
5. tuned signature; (detail / hgweb)
6. misc tuning and clarification; (detail / hgweb)
7. proper treatment of axm_proof/oracle_proof like a closed proof constant, e.g. relevant for proof reconstruction of List.list.full_exhaustive_list.simps; (detail / hgweb)
8. clarified oracle_proof; (detail / hgweb)
9. tuned; (detail / hgweb)
10. tuned; (detail / hgweb)
11. tuned; (detail / hgweb)
12. clarified signature; (detail / hgweb)
13. tuned signature; (detail / hgweb)
14. more compact XML representation; (detail / hgweb)
15. proper generalize_proof: schematic variables need to be explicit in the resulting proof term (for shrink/reconstruct operation); (detail / hgweb)
16. tuned; (detail / hgweb)
17. tuned -- more direct ML expressions; (detail / hgweb)
18. clarified modules; (detail / hgweb)
19. tuned whitespace; (detail / hgweb)
20. more accurate treatment of propositions within proof terms, but these are ultimately ignored for performance reasons; (detail / hgweb)
21. unused; (detail / hgweb)
22. document antiquotations + clarify porting text slightly (detail / hgweb)

Started by an SCM change

This run spent:

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