Changes

Summary

1. strict_sorted now an abbreviation
2. explicit type class operations for type-specific implementations
3. obsolete
4. added lemmas map_ran_Cons_sel and (length|map_fst)_map_ran
5. merged
6. generalized type
7. basic setup of Isabelle setup tool --- pure Java, no dependencies;
8. merged
9. guess package more directly;
10. merged
11. Just one lemma
12. proper support for macOS/Rosetta: let "uname -m" report arm64 instead of x86_64;
13. clarified platforms;
14. merged
15. proper jEdit.props (amending ff716ecb0805);
16. update to gmp-6.2.1, with support for arm64-darwin;
17. clarified platforms;
18. clarified options: implicitly support both x86_64 and arm64;
19. tuned whitespace;
20. centralized more lemmas
21. avoid Fun.swap
22. guide is out of focus
23. proper build for fresh target directory (amending d9823224fcfe);
24. put more resources into jedit_build component;
25. more brackets (see f6b453449cc6);
26. more brackets;
27. proper settings variable, amending 6e85281177df;
28. merged
29. tuned proofs --- avoid z3, which is absent on arm64-linux;
30. proper condition: z3 could be absent, e.g. on arm64-linux;
31. build auxiliary jEdit component in Isabelle/Scala; clarified directory layout;
32. separate component for idea-icons.jar, from jedit_build (see also ff0e0bb81597);
33. tuned message;
34. clarified signature;
35. tuned signature;
36. more elementary swap

Summary

1. strict_sorted now an abbreviation
2. merged
3. deleted needless material
4. explicit type class operations for type-specific implementations
5. next step to phase out ancient numerals
6. more small simplifications
7. merged
8. fixed some latex; tried the alternative definition of Ramsey
9. Trying out Ramsey_eq for simpler proofs
10. more tiny tweaks
11. centralized more lemmas
12. avoid Fun.swap
13. guide is out of focus
14. Relational_Minimum_Spanning_Trees: refactoring Boruvka.thy
15. more elementary swap