#996 (Aug 28, 2019, 1:49:15 AM)

1. removed unused lemma, generalized, reduced dependencies (detail / hgweb)
2. fixed typo (detail / hgweb)
3. moved lemmas; reduced dependencies of Lipschitz (detail / hgweb)
4. explicit instance real::ordered_real_vector before subclass in ordered_euclidean_space (detail / hgweb)
5. merged (detail / hgweb)
6. moved lemmas (detail / hgweb)
7. moved basic theorem (detail / hgweb)
8. proper positions for 'termination' command (see also 5549e686d6ac); (detail / hgweb)
9. tuned names -- proper scopes; (detail / hgweb)
10. added system option "execution_eager": potentially reduce resource requires for "isabelle mmt_import" (smaller subgraphs are finished and disposed earlier); (detail / hgweb)

Started by an SCM change

This run spent:

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