--- 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 |