# HG changeset patch
# User desharna
# Date 1744631868 -7200
# Node ID 05fe696cd40b080e771354c9c2aa19a863513f5d
# Parent  f72b374b6a6995fca856badb16df13d484018c7e
tuned

diff -r f72b374b6a69 -r 05fe696cd40b src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Sun Apr 13 23:01:03 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Mon Apr 14 13:57:48 2025 +0200
@@ -14,21 +14,21 @@
     SMT_Verit of string
 
   datatype proof_method =
-    Metis_Method of string option * string option * string list |
-    Meson_Method |
-    SMT_Method of SMT_backend |
-    SATx_Method |
+    Algebra_Method |
     Argo_Method |
+    Auto_Method |
     Blast_Method |
-    Simp_Method |
-    Auto_Method |
     Fastforce_Method |
     Force_Method |
+    Linarith_Method |
+    Meson_Method |
+    Metis_Method of string option * string option * string list |
     Moura_Method |
-    Linarith_Method |
+    Order_Method |
     Presburger_Method |
-    Algebra_Method |
-    Order_Method
+    SATx_Method |
+    Simp_Method |
+    SMT_Method of SMT_backend
 
   datatype play_outcome =
     Played of Time.time |