#950 (Jun 5, 2019, 12:50:11 AM)

1. tuned; (detail / hgweb)
2. tuned; (detail / hgweb)
3. backout 34bc296374ee -- affects the raw_induct rule, e.g. relevant for AFP/Imperative_Insertion_Sort; (detail / hgweb)
4. unused; (detail / hgweb)
5. tuned messages; (detail / hgweb)
6. proper context; (detail / hgweb)
7. misc tuning and clarification, notably wrt. flow of context; (detail / hgweb)
8. proper context; (detail / hgweb)
9. proper Proof_Context.export_morphism corresponding to Proof_Context.augment (see 7f568724d67e); (detail / hgweb)
10. unused; (detail / hgweb)
11. misc tuning and clarification, notably wrt. flow of context; (detail / hgweb)
12. proper context; (detail / hgweb)
13. proper Proof_Context.export_morphism corresponding to Proof_Context.augment (see 7f568724d67e); (detail / hgweb)

Started by an SCM change

This run spent:

• 9.9 sec waiting;
• 1 hr 17 min build duration;
• 1 hr 17 min total from scheduled to completion.