# HG changeset patch
# User desharna
# Date 1710932158 -3600
# Node ID 6a3212bedfade5eda7a9a7dc20b43f376aa51056
# Parent  5e85ea359563095a6a143bfb45d4b215ed760a8b
added Mirabelle action "order"

diff -r 5e85ea359563 -r 6a3212bedfad NEWS
--- 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.
diff -r 5e85ea359563 -r 6a3212bedfad src/HOL/Mirabelle.thy
--- a/src/HOL/Mirabelle.thy	Wed Mar 20 11:11:04 2024 +0100
+++ b/src/HOL/Mirabelle.thy	Wed Mar 20 11:55:58 2024 +0100
@@ -19,6 +19,7 @@
 \<close>
 
 ML_file \<open>Tools/Mirabelle/mirabelle_arith.ML\<close>
+ML_file \<open>Tools/Mirabelle/mirabelle_order.ML\<close>
 ML_file \<open>Tools/Mirabelle/mirabelle_metis.ML\<close>
 ML_file \<open>Tools/Mirabelle/mirabelle_presburger.ML\<close>
 ML_file \<open>Tools/Mirabelle/mirabelle_quickcheck.ML\<close>