Changes

Summary

1. provide component naproche-20211211;
2. merged
3. more Mailman archives;
4. more Mailman content;
5. clarified signature;
6. tuned metis to use map_index
7. merged
8. fixed HOL-TPTP
9. tuned vars_of_iterm
10. fixed TPTP generation of multi-arity expressions
11. proper handling of Hilbert choice in TFX logics
12. proper tptp_builtins
13. reused Sledgehammer code to parse parameters of sledgehammer action in Mirabelle
14. proper proxy for Hilbert choice in TPTP output
15. proper polymorphism for TH1 format in Sledgehammer
16. refactored $ite and $let configuration and added dummy_thf_reduced prover
17. tuned TPTP file names generated by Sledgehammer
18. tuned SMT-Lib file names generated by Mirabelle
19. added support for higher-order SMT proof search in Sledgehammer
20. separated FOOL from $ite/$let in TPTP output
21. missing latex font
22. Rewrite: added links to docu, made more prominent
23. discontinued old-style {* verbatim *} tokens;
24. tuned proof;
25. isabelle update_cartouches;
26. more symbolic latex_output via XML (using YXML within text);
27. tuned signature: remove unused;
28. prefer symbolic Latex.environment (typeset in Isabelle/Scala);
29. tuned signature;
30. clarified corner cases of syntax;
31. clarified Parse.embedded_ml: follow documentation (8baf2e8b16e2);
32. a slightly simpler proof

Summary

1. merged
2. generalized standard formula redundancy out of standard redundancy
3. merged
4. discontinued Parse.text;
5. discontinued old-style {* verbatim *} tokens;
6. weakened locale assumptions: wfP implies asymp
7. Add papers to metadata.
8. refactored Standard_Redundancy_Criterion to not use ordering type classes
9. isabelle update_cartouches;
10. removed obsolete "extend" operation;
11. more symbolic latex_output via XML (using YXML within text); re-use existing Latex.output_markup;
12. prefer symbolic Latex.environment (typeset in Isabelle/Scala);
13. tuned signature;