--- a/NEWS Wed Mar 20 11:11:04 2024 +0100
+++ b/NEWS Wed Mar 20 11:55:58 2024 +0100
@@ -43,11 +43,13 @@
. 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;
-the related option "proof_method" was removed. Proof reconstruction is
-supported directly by Sledgehammer and should be used instead. For more
-information, see Sledgehammer's documentation relating to
-"preplay_timeout". INCOMPATIBILITY.
+* Mirabelle:
+ - Removed proof reconstruction from "sledgehammer" action;
+ the related option "proof_method" was removed. Proof reconstruction is
+ supported directly by Sledgehammer and should be used instead. For
+ more information, see Sledgehammer's documentation relating to
+ "preplay_timeout". INCOMPATIBILITY.
+ - Added the action "order" testing the proof method of the same name.
* Explicit type class for discrete_linear_ordered_semidom for integral
semidomains with a discrete linear order.