Changes

Summary

1. updated documentation to current matter of affairs
2. unused;
3. clarified signature;
4. merged
5. added Isabelle identification to Mirabelle output
6. uniformized fact selection for ATP and SMT in Sledgehammer
7. provide cache for slow computations;
8. used max_facts and fact_filter from slice for both ATP and SMT in sledgehammer
9. more operations;
10. more liberal parsing of Sledgehammer options to allow empty lists (as suggested by Larry Paulson)
11. more robust TSTP proof parsing
12. added possibility of extra options to SMT slices

Summary

1. merge from afp-2021-1
2. avoid conflict with index.html in generated html
3. New entry: FO_Theory_Rewriting
4. Improve consistency of type-variables in WOOT_Strong_Eventual_Consistency. + Remove obsolete e-mail from notification mailing list.
5. Improve proofs for Interpolation_Polynomials_HOL_Algebra. Reduced the number of apply scripts used.
6. Correct date.
7. deleted a lemma that's in the devel library
8. Cleanup and new results.
9. moved theorems into Matrix.thy
10. merge of AFP 2021-1
11. New AFP entry: Equivalence_Relation_Enumeration
12. new entry: LP_Duality
13. cosmetic tweaks
14. sitegen and metadata for Young's inequality
15. new entry: Young's inequality
16. metadata for Quasi_Borel_Spaces, sitegen
17. new entry: Quasi_Borel_Spaces
18. sitegen for FOL_Seq_Calc2
19. new entry FOL_Seq_Calc2
20. tweak: corollary that the ln also yields irrational numbers
21. New entry: Interpolation_Polynomials_HOL_Algebra
22. Finally remembered to run sitegen
23. Fixed the meta data in the abstract as well
24. Eliminated the references to SOS (which is no longer used) and changed to the document style to "article".
25. typo
26. typo
27. New entry Irrationals_From_THEBOOK
28. new entry Median_Method
29. Actuarial Mathematics website
30. New entry Actuarial_Mathematics