#1019 (Apr 11, 2024, 2:15:11 PM)

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

Started by an SCM change

This run spent:

• 7.9 sec waiting;
• 5 hr 11 min build duration;
• 5 hr 12 min total from scheduled to completion.

• Isabelle_Marries_Dirac