equal
deleted
inserted
replaced
226 * Mirabelle: |
226 * Mirabelle: |
227 - Added session to output directory structure. Minor INCOMPATIBILITY. |
227 - Added session to output directory structure. Minor INCOMPATIBILITY. |
228 |
228 |
229 * Metis: |
229 * Metis: |
230 - Made clausifier more robust in the face of nested lambdas. |
230 - Made clausifier more robust in the face of nested lambdas. |
|
231 Minor INCOMPATIBILITY. |
|
232 |
|
233 * Sledgehammer: |
|
234 - Added refutational mode to find likely unprovable conectures. It is |
|
235 enabled by default in addition to the usual proving mode and can be |
|
236 enabled or disabled using the 'refute' option. |
231 |
237 |
232 |
238 |
233 *** ML *** |
239 *** ML *** |
234 |
240 |
235 * Operations for Zstd compression (via Isabelle/Scala): |
241 * Operations for Zstd compression (via Isabelle/Scala): |