Changes

Summary

1. clarified antiquotations;
2. merged
3. clarified antiquotations; some comments concerning odd "- numeral";
4. clarified antiquotations;
5. clarified antiquotations;
6. merged
7. tuned TPTP parsing of THF function application
8. clarified examples;
9. repaired slip
10. merged
11. updated to Zipperposition 2.1
12. fixed veriT environment variable in sledgehammer's documentation
13. avoid overlapping PIDE markup (amending bb25ea271b15);
14. recover some Linux test, using virtual machine node (Ubuntu 20.04, 4 cores, 16 GB);
15. clarified antiquotations;
16. merged
17. clarified antiquotations;
18. clarified antiquotations;
19. clarified antiquotations;
20. clarified antiquotations;
21. clarified antiquotations;
22. clarified positions, notably for ML compiler errors;
23. clarified message;
24. proper default for Sledgehammer GUI panel;
25. tuned antiquotations;
26. more convenient ML arguments: avoid excessive nesting of cartouches;
27. outer syntax: support for control-cartouche tokens;
28. merged
29. An example
30. prefer veriT over Z3 in sledgehammer
31. added Zipperposition to sledgehammer's default provers
32. provide zipperposition-2.1 (still unused);
33. tuned docs
34. merged
35. improper proof command 'guess' moved to separate theory "Pure-ex.Guess";
36. NOT is part of syntax bundle also

Summary

1. repaired slip
2. feat(SpecCheck) folder renaming, types for tests
3. tuned
4. mproper proof command 'guess' moved to separate theory "Pure-ex.Guess", according to Isabelle/b49bd5d9041f;