Changes

Summary

1. merged
2. discontinued fragile operation;
3. more robust operations: avoid somewhat fragile Document.Node.Name.master_dir_path;
4. tuned whitespace;
5. tuned;
6. avoid somewhat fragile Document.Node.Name.master_dir_path;
7. clarified signature: avoid somewhat fragile Document.Node.Name.master_dir_path;
8. tuned;
9. clarified modules;
10. tuned;
11. tuned;
12. clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;
13. tuned signature: avoid too many aliases (see also 72daee8a39ca);
14. clarified modules;
15. merged
16. strengthened and renamed lemmas asym_on_iff_irrefl_on_if_trans and asymp_on_iff_irreflp_on_if_transp
17. Fixed a couple of simple_path occurrences
18. merged
19. Tidying up of paths, introducing "loop_free" as a separate predicate in the definition of "simple_path"