Changes

Summary

1. tuned signature, following Url.append_path;
2. merged
3. more robust, for the sake of very rare duplicate files: src/Doc/Prog_Prove/MyList.thy and $AFP/Case_Labeling/util.ML;
4. store session sources within build database: timing e.g. 150ms for HOL and < 50ms for common sessions; enforce rebuild of Isabelle/ML to update build databases;
5. tuned signature;
6. tuned;
7. tunes signature;
8. clarified signature;
9. tuned signature;
10. more systematic Sessions.illegal_theory, based on File_Format.theory_excluded;
11. tuned;
12. unused;
13. tuned;
14. clarified modules;
15. tuned: no need to map master_dir, which does not participate in comparison;
16. tuned signature;
17. tuned signature;
18. tuned comments;
19. clarified signature;
20. tuned;
21. removed an unfortunate sledgehammer command
22. A couple of patches
23. Big simplifications of old proofs