Changes

Summary

1. tweaked time functions for median-of-medians selection in HOL-Data_Structures
2. merged
3. rename \undef to \undefined to avoid problems with MacTeX 2014 or Ubuntu 24.04 beta;
4. Tiny tweaks to proofs
5. A bit of new material about type class "infinite", from Eval_FO
6. avoid Scala if-expressions and thus make it work both for -new-syntax or -old-syntax;
7. proper Scala code for String.literal_of_asciis: avoid ambiguity of ("" ++ ...);
8. adjust generated Scala to make it work with scalac -old-syntax and -new-syntax, although the latter is not regularly tested;
9. Add entry on Sketch_and_Explore to CONTRIBUTORS
10. moved over material from the AFP to HOL, HOL-Computational_Algebra, and HOL-Number_Theory
11. more portable: prefer official JDBC operation DatabaseMetaData.getColumns();
12. tuned signature;