equal
deleted
inserted
replaced
108 |
108 |
109 * Strong congruence rules (with =simp=> in the premises) for constant f |
109 * Strong congruence rules (with =simp=> in the premises) for constant f |
110 are now uniformly called f_cong_simp, in accordance with congruence |
110 are now uniformly called f_cong_simp, in accordance with congruence |
111 rules produced for mappers by the datatype package. INCOMPATIBILITY. |
111 rules produced for mappers by the datatype package. INCOMPATIBILITY. |
112 |
112 |
113 * Sledgehammer: The URL for SystemOnTPTP, which is used by remote |
113 * Sledgehammer: |
114 provers, has been updated. |
114 - The URL for SystemOnTPTP, which is used by remote provers, has |
|
115 been updated. |
|
116 - The machine-learning-based filter MaSh has been optimized to take |
|
117 less time (in most cases). |
115 |
118 |
116 * SMT: reconstruction is now possible using the SMT solver veriT. |
119 * SMT: reconstruction is now possible using the SMT solver veriT. |
117 |
120 |
118 * HOL-Library.Simps_Case_Conv: case_of_simps now supports overlapping |
121 * HOL-Library.Simps_Case_Conv: case_of_simps now supports overlapping |
119 and non-exhaustive patterns and handles arbitrarily nested patterns. |
122 and non-exhaustive patterns and handles arbitrarily nested patterns. |