equal
deleted
inserted
replaced
130 INCOMPATIBILITY: in cases explicitly referring to K_record. |
130 INCOMPATIBILITY: in cases explicitly referring to K_record. |
131 |
131 |
132 * Metis prover is now an order of magnitude faster, and also works |
132 * Metis prover is now an order of magnitude faster, and also works |
133 with multithreading. |
133 with multithreading. |
134 |
134 |
|
135 * Sledgehammer no longer produces structured proofs by default. To enable, |
|
136 declare [[sledgehammer_full = true]]. Attributes reconstruction_modulus, |
|
137 reconstruction_sorts renamed sledgehammer_modulus, sledgehammer_sorts. |
|
138 INCOMPATIBILITY. |
135 |
139 |
136 *** ZF *** |
140 *** ZF *** |
137 |
141 |
138 * Renamed theories: |
142 * Renamed theories: |
139 |
143 |