Changes

Summary

1. things need to be ugly
2. merged
3. sorted as an abbreviation
4. mere abbreviation for logical alias
5. avoid unexpected output+behaviour when CDPATH is set
6. recover some Linux test, using old macbroy2 as i21of4 (Ubuntu 20.04);
7. avoid perl;
8. tuned signature --- following hints by IntelliJ IDEA;
9. ignore session build timeout, notably in AFP;
10. check timeout_ignored as in ML, before applying timeout_scale;
11. merged
12. proper build of required session images vs. build with Mirabelle presentation;
13. reactive "sledgehammer";
14. reactive "sledgehammer_filter": statically correct, but untested (no proof_file);
15. clarified command-line;
16. clarified signature; supporess empty results;
17. clarified signature;
18. clarified log content;
19. reimplemented Mirabelle as Isabelle/ML presentation hook + Isabelle/Scala tool, but sledgehammer is still inactive;
20. tuned;
21. unused;
22. unused (see 8ffc607c345d);
23. clarified signature: provide access to previous state;
24. clarified signature (see Scala version);
25. tuned signature;
26. avoid duplicate loading of ML file;

Summary

1. PATCH to Auto2 (for sorted) by Bohua, pending a permanent generalisation of "properties"
2. fixed two more "sorted" errors
3. fixed two "sorted" issues
4. merged
5. changes for "sorted" as an abbreviation
6. mere abbreviation for logical alias
7. eliminated odd clone (see Isabelle/caa5a257d3ed);