--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Fri Jul 12 21:13:57 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Fri Jul 12 21:14:54 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
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Fri Jul 12 21:13:57 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Fri Jul 12 21:14:54 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 [] [] = ""
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Fri Jul 12 21:13:57 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Fri Jul 12 21:14:54 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)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Fri Jul 12 21:13:57 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_try0.ML Fri Jul 12 21:14:54 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))*)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jul 12 21:13:57 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Jul 12 21:14:54 2013 +0200
@@ -4,8 +4,6 @@
General-purpose functions used by the Sledgehammer modules.
*)
-infix 1 |>! #>!
-
signature SLEDGEHAMMER_UTIL =
sig
val sledgehammerN : string
@@ -33,12 +31,6 @@
val max : ('a * 'a -> order) -> 'a -> 'a -> 'a
val max_option : ('a * 'a -> order) -> 'a option -> 'a option -> 'a option
val max_list : ('a * 'a -> order) -> 'a list -> 'a option
-
- (** debugging **)
- val print_timing : ('a -> 'b) -> 'a -> 'b
- (* infix versions of print_timing; meant to replace '|>' and '#>' *)
- val |>! : 'a * ('a -> 'b) -> 'b
- val #>! : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c
end;
structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
@@ -173,14 +165,4 @@
fun max_list ord xs = fold (SOME #> max_option ord) xs NONE
-(** debugging **)
-fun print_timing f x =
- Timing.timing f x
- |>> Timing.message
- |>> warning
- |> snd
-
-fun x |>! f = print_timing f x
-fun (f #>! g) x = x |> f |>! g
-
end;