Changes

Summary

1. obsolete (see f3378101f555);
2. merged
3. more direct unlimited smt_timeout; update of certificates: generated command-line options are part of input / digest;
4. clarified smt: support Timeout.ignored and Timeout.scale_time;
5. clarified timeouts in Isabelle/ML;
6. tuned --- more elementary Time operations;
7. removed unused/pointless operation: Time.start is the load/init time of this Scala module;
8. obsolete;
9. clarified signature --- augment existing structure Time;
10. rebuild SMT certificates from scratch;
11. added lemmas (sublist|prefix|suffix)_list_all
12. added lemmas takeWhile_is_prefix, suffix_dropWhile, and sublist_(take|drop)While
13. added lemmas list_all_(take|drop)I and list_all_(take|drop)WhileI
14. typo
15. merged
16. added upper bound on monomorphisation duplicate instances
17. tuned best_slices in atp_config
18. tuned exec field in atp_config
19. removed junk;
20. tuned proofs;
21. enforce full build, after significant changes in Isabelle/Scala;
22. clarified compiler options: show relevant warnings;
23. tuned --- avoid compiler warnings;
24. clarified signature --- fewer warnings;
25. clarified signature --- fewer warnings;
26. tuned --- fewer warnings;
27. more robust ordering (see also 88c96e836ed6);
28. proper scala.collection.immutable;
29. tuned --- fewer warnings;
30. tuned --- fewer warnings;
31. tuned;
32. tuned --- fewer warnings;
33. tuned --- fewer warnings;
34. tuned --- fewer warnings;
35. tuned --- fewer warnings;
36. more robust error;
37. tuned --- fewer warnings;
38. tuned --- fewer warnings;
39. tuned --- fewer warnings;
40. updated to scala-2.13.5 (with scala-swing_2.13-3.0.0);
41. slightly more efficient Term.fastype_of (only little impact in regular applications);
42. reduced dependencies on theory List_Permutation
43. Merge
44. reverted simprule status on a new lemma
45. merged
46. tiny bit of lemma hacking
47. tuned --- fewer warnings;
48. tuned --- fewer warnings;
49. tuned --- avoid deprecated conversions between certain number type;
50. tuned --- avoid deprecated Predef.any2stringadd;
51. tuned --- silence odd warning;
52. tuned --- fewer warnings;
53. tuned --- fewer warnings;
54. tuned --- fewer warnings;
55. tuned --- fewer warnings;
56. clarified signature, according to Isabelle/Scala;
57. download more directly, via means of JVM;
58. download on separate thread;
59. clarified signature;
60. tuned;
61. proper relative path (see also df49ca5da9d0, 5b15eee1a661, etc.);
62. tuned signature;
63. NEWS
64. lemma diffusion
65. more connections between mset _ = mset _ and permutations
66. dissolve theory with duplicated name from afp
67. more robust (amending 87403fde8cc3): notably allow symlink to existing directory, which Files.createDirectories does not accept;
68. more Isabelle/ML/Scala operations;
69. more Isabelle/ML/Scala operations;
70. more Isabelle/ML/Scala operations; clarified errors;
71. proper src1, amending 20157c8ab3f3;
72. tuned;
73. proper File.eq, amending df49ca5da9d0;
74. tuned;
75. clarified modules: more like ML;
76. obsolete;
77. tuned;
78. more direct make_directory in ML and Scala, but ssh still requires perl for Windows UNC paths (see a5dbad753552);
79. discontinued somewhat pointless "integrity test of build_history": it fails right now, but also failed to expose spurious incompatibilities when it was working;

Summary

1. tuned
2. Tuned presentation of Buffon's needle
3. tuned
4. reduced dependencies on theory List_Permutation
5. tidied up messy proofs
6. lemma diffusion
7. more connections between mset _ = mset _ and permutations
8. dissolve theory with duplicated name from afp