Changes

Summary

1. tuned proofs -- avoid z3, which is unavailable on arm64-linux;
2. tuned;
3. test version of prespective polyml-5.9;
4. clarified antiquotations;
5. updated for pre-5.9 testing;
6. clarified antiquotations;
7. clarified antiquotations;
8. clarified antiquotations;
9. more robust subgoal addressing;
10. proper subgoal addressing;
11. clarified antiquotations;
12. recursive find_eq, not find_dist;
13. misc tuning and clarification;
14. clarified antiquotations;
15. order_tac: prevent potential bug, improve perf and tracing - We need to be careful when the order operators contain schematic variables, e.g. <= = ccw' ?p.
16. misc tuning and clarification;
17. clarified antiquotations;
18. clarified antiquotations: no need for Thm.beta_conversion, due to Thm.instantiate_beta;
19. clarified antiquotations: no need for Thm.beta_conversion, due to Thm.instantiate_beta;
20. avoid persistence of static context: instantiation arguments should provide proper dynamic context (see also e2e2bc1f9570);
21. added Thm.instantiate_beta; tuned;
22. moved generic implementation into HOL-Main
23. tuned;
24. tuned;
25. clarified antiquotations;
26. clarified antiquotations;
27. discontinued somewhat pointless antiquotations;
28. NEWS;
29. clarified antiquotations, assuming that Drule.instantiate_normalize was merely a historical relic;
30. clarified antiquotations;
31. clarified antiquotations;
32. clarified antiquotations;
33. clarified antiquotations;
34. support for "lemma"; support for "schematic" mode; clarified error position;
35. tuned;
36. local fixes for "lemma" antiquotation;
37. clarified signature;
38. tuned;
39. clarified keywords: major take precedence for commands, but not used for antiquotations; clarified modules;
40. tuned modules;
41. more antiquotations;
42. moved a theorem to a sensible place
43. merged
44. tuned, continuing e955964d89cb;
45. avoid waste of resources due to dynamic simpset (amending 45c09620f726);
46. fix latex
47. clarified modules;
48. more generic bit/word lemmas for distribution
49. merged
50. Added / moved some simple set-theoretic lemmas
51. more CONTRIBUTORS and NEWS;
52. cleanup; add Apple reference
53. refine interface
54. generalized component lookup for syntax and distinctness proofs. added some tracing.
55. merged
56. tuned;
57. more antiquotations;
58. more antiquotations;
59. more robust: genuinely free variables need to be instantiated;
60. tuned comments;
61. clarified errors;
62. tuned;
63. clarified instantiation: local beta reduction after substitution, as for Envir.expand_term_defs;
64. tuned;
65. clarified signature -- avoid clones;
66. Refinement of partitions
67. avoid persistence of static context: instantiation arguments should provide proper dynamic context;
68. more antiquotations;
69. more markup;
70. clarified name, syntax, messages;
71. more antiquotations;
72. more control symbols;
73. tuned signature;
74. ML antiquotations to instantiate types/terms/props;
75. tuned;
76. clarified modules;
77. clarified modules;
78. clarified modules;
79. discontinued obsolete "val extend = I" for data slots;
80. clarified modules;
81. clarified modules;
82. clarified signature;
83. tuned;
84. clarified keywords and reports;
85. clarified signature;
86. merged
87. proper veriT --max-time option
88. refactored tptp_builtins in Sledgehammer
89. merged
90. tuned ML --- clarified use of context; tuned message;
91. tuned --- fewer clones;
92. updated to jEdit plugin Highlight 2.5;
93. proper tactic combinator;
94. proper file headers;
95. clarified context; clarified modules;
96. more accurate treatment of context;
97. updated email address
98. removed some 'private' modifiers from HOL-Computational_Algebra
99. merged
100. merged
101. more robust Variable.revert_bounds (see also b12f2cef3ee5);
102. more accurate treatment of context;
103. tuned -- proper names/scopes for contexts;
104. clarified context;
105. clarified context;
106. tuned;
107. unused;
108. more accurate treatment of context; declare generated bounds for the sake of recdef, which has variables leaking from local context;
109. isabelle regenerate_cooper;
110. revert bbfed17243af, breaks HOL-Proofs extraction;
111. tuned;
112. tuned;
113. proper p' instead of p (amending 52c7c42e7e27);
114. proper context for Goal.prove_internal;
115. discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily; Simplifier and equational conversions demand a proper proof context;
116. more accurate treatment of context, notably for nested Goal.proof / SUBPROOF;
117. tuned;
118. tuned;
119. tuned;
120. spelling;
121. clarified context;
122. clarified signature;
123. tuned Vampire configuration to use TFX in Sledgehammer

Summary

1. updated metadata for Count_Complex_Roots
2. corrected the timeout for CZH_Universal_Constructions
3. CZH: further results about comma categories and Kan extensions, a variety of other minor amendments
4. more generic bit/word lemmas for distribution
5. Fixing a name clash between two different "restrict" operators
6. Merged
7. solved the roots-on-the-border problem
8. split Count_Complex_Roots
9. more realistic timeout;
10. clarified signature, according to Isabelle/ccf599864beb;
11. back to dedicated separate shift operations for infix syntax; more default simp rules on closed numeric expressions
12. modify JinjaDCI
13. modify JinjaDCI
14. Merged.
15. Various tuning that for some reason didn't get merged from my master branch.
16. A spot of polishing
17. Merged.
18. Update metadata to reflect changes made in July, 2021.
19. Add a revision note concerning material added in July, 2021.
20. tuned signature, according to Isabelle/042041c0ebeb;
21. Merged.
22. Sync with my development repo.
23. Adjust Imperative List/Map/Set Specification for more lenient next operation This allows implementations of this iterator specification to make use of temporary variables for obtaining the next element of the list/set/map. This is required by some and especially more general iterators.
24. discontinued obsolete "val extend = I" for data slots;
25. tuned;
26. merged
27. metadata update for MFODL_Monitor_Optimized
28. fixed a mistake in MFODL_Monitor_Optimized
29. merge
30. adjusted Virtual-Substitution from 2021 to devel
31. merge of AFP 2021
32. fixed duplicate "and"
33. sitegen for Virtual_Substitution
34. new entry: Virtual Substitution
35. updated website/email address
36. modifications in Jinja and DOminance_CHK
37. modifications in Jinja and Dominance_CHK
38. modifications in Jinja and Dominance_CHK
39. merged
40. adapted to Term.dest_abs_global / Logic.dest_all_global (e.g. Isabelle/f07761ee5a7f);
41. more accurate treatment of context;
42. more accurate treatment of context;
43. more accurate treatment of context;
44. tuned -- proper names/scopes for contexts;
45. tuned proofs;
46. more accurate treatment of context;
47. more accurate treatment of context;
48. proper antiquotations;
49. tuned messages;
50. more maintainable Isabelle/ML: proper signatures, proper names/scopes for contexts; tuned whitespace;
51. dead code!?
52. clarified signature, following Isabelle/de4f151c2a34;