Changes

Summary

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