#829 (Dec 30, 2018, 12:50:11 AM)

1. split off theorems involving classes below metric_space and real_normed_vector (detail / hgweb)
2. merged (detail / hgweb)
3. merged (detail / hgweb)
4. tuned analysis manual (detail / hgweb)
5. tuned signature; (detail / hgweb)
6. merged (detail / hgweb)
7. clarified signature, notably cascade of dump_options, deps, resources, session; (detail / hgweb)
8. unused; (detail / hgweb)
9. clarified signature; (detail / hgweb)
10. clarified errors, according to Isabelle/MMT;
    tuned signature; (detail / hgweb)
11. tuned, according to Isabelle/MMT; (detail / hgweb)
12. clarified options: ensure consolidated Node_Status and thus percentage = 100% for progress; (detail / hgweb)
13. tuned; (detail / hgweb)
14. merged (detail / hgweb)
15. more capitalization (detail / hgweb)
16. capitalize proper names in lemma names (detail / hgweb)
17. explicit dependencies for includes (detail / hgweb)
18. more correct handling of symbols for includes (detail / hgweb)

Started by an SCM change

This run spent:

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