Changes

Summary

1. clarified modules;
2. clarified check (refining fc828f64da5b): etc/settings or etc/components is not strictly required according to "init_component", and notable components only have session ROOTS (e.g. AFP/thys);
3. tuned;
4. more thorough update of required files (amending 1529c3eb6bac);
5. clarified examples;
6. tuned proofs;
7. misc tuning --- following hints by Jørgen Villadsen (see also 1ce1bc9ff64a);
8. tuned --- reduced source complexity;
9. proper usage (amending f7ea394490f5);
10. merged, resolving minor conflict;
11. allow build session setup, e.g. for protocol handlers;
12. unused;
13. tuned --- potentially more robust (e.g. session.phase_changed vs. isabelle_process.terminated);
14. clarified signature;
15. removed pointless option (see 3d0952893db8);
16. tuned --- avoid redundant future tasks from already loaded theories;
17. no comment --- topological order appears to be fine since 04-Mar-2013;
18. more predictable sequential presentation (2f9877db82a1), without somewhat pointless result_ord (e7fab0b5dbe7);
19. moved stride option from sledgehammer action to main mirabelle
20. merged
21. new lemmas mostly about paths
22. lexorders the locale way
23. more accurate export morphism enables proper instantiation by interpretation

Summary

1. more specific export_files: omit recent additions ("document", "PIDE", etc.);
2. grouped lemmas
3. bundles for traditional infix syntax