# HG changeset patch
# User wenzelm
# Date 1709892584 -3600
# Node ID 80a30835f48f4be4e765f0e0ab5466fdefbde6c9
# Parent  5dd2a771811e44f3908b4987f5e0c204c3e132f4
update NEWS;

diff -r 5dd2a771811e -r 80a30835f48f NEWS
--- 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;