# HG changeset patch
# User smolkas
# Date 1373656054 -7200
# Node ID d6f2a7c196f7c263a9a899fae16c14595fbc855c
# Parent  94fbc50a6757ee4bdb3564ce6c2177b62ea08656
added blast, force

diff -r 94fbc50a6757 -r d6f2a7c196f7 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Fri Jul 12 20:28:34 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Fri Jul 12 21:07:34 2013 +0200
@@ -125,7 +125,9 @@
               SimpM => Simplifier.asm_full_simp_tac
             | AutoM => (fn ctxt => K (Clasimp.auto_tac ctxt))
             | 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
 
 
diff -r 94fbc50a6757 -r d6f2a7c196f7 src/HOL/Tools/Sledgehammer/sledgehammer_print.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Fri Jul 12 20:28:34 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Fri Jul 12 21:07:34 2013 +0200
@@ -175,7 +175,9 @@
         SimpM => "simp"
       | AutoM => "auto"
       | FastforceM => "fastforce"
+      | ForceM => "force"
       | ArithM => "arith"
+      | Blast => "blast"
       | _ => raise Fail "Sledgehammer_Print: by_method")
 
     fun using_facts [] [] = ""
diff -r 94fbc50a6757 -r d6f2a7c196f7 src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Fri Jul 12 20:28:34 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Fri Jul 12 21:07:34 2013 +0200
@@ -29,7 +29,9 @@
     SimpM |
     AutoM |
     FastforceM |
-    ArithM
+    ForceM |
+    ArithM |
+    BlastM
 
   (* legacy *)
   val By_Metis : facts -> byline
@@ -94,7 +96,9 @@
   SimpM |
   AutoM |
   FastforceM |
-  ArithM
+  ForceM |
+  ArithM |
+  BlastM
 
 (* legacy *)
 fun By_Metis facts = By (facts, MetisM)
diff -r 94fbc50a6757 -r d6f2a7c196f7 src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML	Fri Jul 12 20:28:34 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML	Fri Jul 12 21:07:34 2013 +0200
@@ -23,7 +23,7 @@
 fun variants (Let _) = raise Fail "Sledgehammer_Try0: variants"
   | variants (Prove (qs, xs, l, t, subproofs, By (facts, _))) =
       let
-        val methods = [SimpM, AutoM, FastforceM, ArithM]
+        val methods = [SimpM, FastforceM, AutoM, ArithM, ForceM, BlastM]
         fun step method = Prove (qs, xs, l, t, subproofs, By (facts, method))
         (*fun step_without_facts method =
           Prove (qs, xs, l, t, subproofs, By (no_facts, method))*)