equal
deleted
inserted
replaced
34 |
34 |
35 * Commands 'inductive_cases', 'inductive_simps', 'case_of_simps', |
35 * Commands 'inductive_cases', 'inductive_simps', 'case_of_simps', |
36 'simps_of_case' now print results like 'theorem'. |
36 'simps_of_case' now print results like 'theorem'. |
37 |
37 |
38 * Sledgehammer |
38 * Sledgehammer |
39 - Update of bundled prover: |
39 - Update/rebuild of bundled provers: |
40 + Vampire 4.8 HO - Sledgehammer schedules (2023-10-19) |
40 . E prover 3.0, with native ARM64 executables |
|
41 . Vampire 4.8 HO - Sledgehammer schedules (2023-10-19) |
|
42 . veriT 2021.06.1-rmx - rebuild for arm64-linux |
|
43 . Z3 4.4.1 for arm64-linux has been removed: unreliable, unstable. |
41 - New implementation of moura tactic. INCOMPATIBILITY. |
44 - New implementation of moura tactic. INCOMPATIBILITY. |
42 |
45 |
43 * Mirabelle: Removed proof reconstruction from "sledgehammer" action; |
46 * Mirabelle: Removed proof reconstruction from "sledgehammer" action; |
44 the related option "proof_method" was removed. Proof reconstruction is |
47 the related option "proof_method" was removed. Proof reconstruction is |
45 supported directly by Sledgehammer and should be used instead. For more |
48 supported directly by Sledgehammer and should be used instead. For more |