Changes

Summary

1. clarified signature;
2. tuned signature;
3. clarified signature;
4. merged
5. prefer Isabelle.Bytes, based on ShortByteString;
6. tuned;
7. tuned signature;
8. tuned signature: more generic operations;
9. prefer UTF8 implementation from Data.Text.Encoding (foreign C); clarified signatures and modules;
10. documented Mirabelle_Sledgehammer's new keep semantics
11. changed Mirabelle_Sledgehammer keep option from path to boolean
12. added automatic uniform stride option to Mirabelle
13. fixed HOL-ex following a5bab59d580b
14. added support for TFX $let to Sledgehammer's TPTP output
15. merged
16. fixed TFX generation when universal quantifier is used as term
17. merged
18. various improvements of "isabelle scala_project";
19. support for native symlinks on Windows;
20. tuned Mirabelle's theory selection
21. clarified signature;
22. clarified signature;
23. updated for Isabelle2021 release;
24. back to stackage lts-17.10, to make this work on vmnipkow9 (Windows Server 2012 R2);
25. update to Haskell stack-2.7.3 and stackage lts-17.15;
26. clarified version: Apple now counts like 11, 12, ...;

Summary

1. cleaner presentation of analysis theorems in preliminaries
2. Update to new Epistemic_Logic.thy
3. Avoid typedefs
4. Clean: set AFP standard document options
5. Clean: re-add to chapter AFP
6. merge from afp-2021
7. Finitely_Generated_Abelian_Groups website
8. new entry Finitely_Generated_Abelian_Groups
9. Added Finitely_Generated_Abelian_Groups to metadata