--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 14:30:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 03 14:35:19 2014 +0100
@@ -103,10 +103,11 @@
fun tac_of_method ctxt (local_facts, global_facts) meth =
Method.insert_tac local_facts THEN'
(case meth of
- Meson_Method => Meson.meson_tac ctxt global_facts
- | Metis_Method (type_enc_opt, lam_trans_opt) =>
+ Metis_Method (type_enc_opt, lam_trans_opt) =>
Metis_Tactic.metis_tac [type_enc_opt |> the_default partial_type_enc]
(the_default default_metis_lam_trans lam_trans_opt) ctxt global_facts
+ | SMT_Method => SMT_Solver.smt_tac ctxt global_facts
+ | Meson_Method => Meson.meson_tac ctxt global_facts
| _ =>
Method.insert_tac global_facts THEN'
(case meth of
@@ -118,8 +119,7 @@
| Force_Method => Clasimp.force_tac ctxt
| Arith_Method => Arith_Data.arith_tac ctxt
| Blast_Method => blast_tac ctxt
- | Algebra_Method => Groebner.algebra_tac [] [] ctxt
- | _ => raise Fail "Sledgehammer_Isar_Preplay: tac_of_method"))
+ | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
(* main function for preplaying Isar steps; may throw exceptions *)
fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, fact_names, _)) =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Feb 03 14:30:16 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Mon Feb 03 14:35:19 2014 +0100
@@ -15,6 +15,8 @@
datatype proof_method =
Metis_Method of string option * string option |
+ Meson_Method |
+ SMT_Method |
Simp_Method |
Simp_Size_Method |
Auto_Method |
@@ -22,7 +24,6 @@
Force_Method |
Arith_Method |
Blast_Method |
- Meson_Method |
Algebra_Method
datatype isar_proof =
@@ -80,6 +81,8 @@
datatype proof_method =
Metis_Method of string option * string option |
+ Meson_Method |
+ SMT_Method |
Simp_Method |
Simp_Size_Method |
Auto_Method |
@@ -87,7 +90,6 @@
Force_Method |
Arith_Method |
Blast_Method |
- Meson_Method |
Algebra_Method
datatype isar_proof =
@@ -108,6 +110,8 @@
Metis_Method (NONE, NONE) => "metis"
| Metis_Method (type_enc_opt, lam_trans_opt) =>
"metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
+ | Meson_Method => "meson"
+ | SMT_Method => "smt"
| Simp_Method => "simp"
| Simp_Size_Method => "simp add: size_ne_size_imp_ne"
| Auto_Method => "auto"
@@ -115,7 +119,6 @@
| Force_Method => "force"
| Arith_Method => "arith"
| Blast_Method => "blast"
- | Meson_Method => "meson"
| Algebra_Method => "algebra")
fun steps_of_isar_proof (Proof (_, _, steps)) = steps
@@ -291,6 +294,7 @@
fun is_direct_method (Metis_Method _) = true
| is_direct_method Meson_Method = true
+ | is_direct_method SMT_Method = true
| is_direct_method _ = false
(* Local facts are always passed via "using", which affects "meson" and "metis". This is