--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Mon Dec 16 09:40:02 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Mon Dec 16 09:48:26 2013 +0100
@@ -105,16 +105,17 @@
fun tac_of_method method type_enc lam_trans ctxt facts =
(case method of
MetisM => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts
+ | MesonM => Meson.meson_tac ctxt facts
| _ =>
Method.insert_tac facts THEN'
(case method of
- SimpM => Simplifier.asm_full_simp_tac
- | AutoM => Clasimp.auto_tac #> K
- | FastforceM => Clasimp.fast_force_tac
- | ForceM => Clasimp.force_tac
- | ArithM => Arith_Data.arith_tac
- | BlastM => blast_tac
- | _ => raise Fail "Sledgehammer_Preplay: tac_of_method") ctxt)
+ SimpM => Simplifier.asm_full_simp_tac ctxt
+ | AutoM => K (Clasimp.auto_tac ctxt)
+ | FastforceM => Clasimp.fast_force_tac ctxt
+ | ForceM => Clasimp.force_tac ctxt
+ | ArithM => Arith_Data.arith_tac ctxt
+ | BlastM => blast_tac ctxt
+ | _ => raise Fail "Sledgehammer_Preplay: tac_of_method"))
(* main function for preplaying Isar steps; may throw exceptions *)
fun preplay_raw _ _ _ _ _ (Let _) = zero_preplay_time
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Mon Dec 16 09:40:02 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Mon Dec 16 09:48:26 2013 +0100
@@ -180,6 +180,7 @@
| ForceM => "force"
| ArithM => "arith"
| BlastM => "blast"
+ | MesonM => "meson"
| _ => raise Fail "Sledgehammer_Print: by_method")
fun using_facts [] [] = ""
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Mon Dec 16 09:40:02 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Mon Dec 16 09:48:26 2013 +0100
@@ -26,7 +26,8 @@
FastforceM |
ForceM |
ArithM |
- BlastM
+ BlastM |
+ MesonM
val no_label : label
val no_facts : facts
@@ -83,7 +84,8 @@
FastforceM |
ForceM |
ArithM |
- BlastM
+ BlastM |
+ MesonM
val no_label = ("", ~1)
val no_facts = ([],[])
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Mon Dec 16 09:40:02 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Mon Dec 16 09:48:26 2013 +0100
@@ -21,7 +21,7 @@
open Sledgehammer_Proof
open Sledgehammer_Preplay
-val variant_methods = [SimpM, AutoM, ArithM, FastforceM, BlastM, ForceM, MetisM]
+val variant_methods = [SimpM, AutoM, ArithM, FastforceM, BlastM, ForceM, MetisM, MesonM]
fun variants_of_step (Let _) = raise Fail "Sledgehammer_Try0: variants_of_step"
| variants_of_step (Prove (qs, xs, l, t, subproofs, (facts, meth))) =