NEWS
changeset 79809 80a30835f48f
parent 79806 ba8fb71587ae
child 79890 80487bd00820
--- a/NEWS	Fri Mar 08 10:57:59 2024 +0100
+++ b/NEWS	Fri Mar 08 11:09:44 2024 +0100
@@ -36,8 +36,11 @@
 'simps_of_case' now print results like 'theorem'.
 
 * Sledgehammer
-  - Update of bundled prover:
-    + Vampire 4.8 HO - Sledgehammer schedules (2023-10-19)
+  - Update/rebuild of bundled provers:
+    . E prover 3.0, with native ARM64 executables
+    . Vampire 4.8 HO - Sledgehammer schedules (2023-10-19)
+    . veriT 2021.06.1-rmx - rebuild for arm64-linux
+    . Z3 4.4.1 for arm64-linux has been removed: unreliable, unstable.
   - New implementation of moura tactic. INCOMPATIBILITY.
 
 * Mirabelle: Removed proof reconstruction from "sledgehammer" action;