#1027 (Oct 10, 2019, 1:38:47 AM)

1. merged (detail / hgweb)
2. tuned; (detail / hgweb)
3. misc tuning and clarification; (detail / hgweb)
4. tuned; (detail / hgweb)
5. tuned -- allow slightly more expensive atomic proofs; (detail / hgweb)
6. clarified signature -- some operations to support fully explicit proof terms; (detail / hgweb)
7. tuned; (detail / hgweb)
8. tuned; (detail / hgweb)
9. proper treatment of sorts; (detail / hgweb)
10. tuned app_types: more direct map_proof_types_same; (detail / hgweb)
11. tuned; (detail / hgweb)
12. generalized parsing, for e.g. Leo-III (detail / hgweb)
13. More theorems about limits, including cancellation simprules (detail / hgweb)
14. Generalised two results concerning limits from the real numbers to type classes (detail / hgweb)
15. formally augmented corresponding rules for field_simps (detail / hgweb)

Started by an SCM change

This run spent:

• 48 min waiting;
• 1 hr 20 min build duration;
• 2 hr 9 min total from scheduled to completion.