# HG changeset patch # User bulwahn # Date 1291629165 -3600 # Node ID 29e5cae935842962bb81a9a71de3e72ab1672835 # Parent 890fefa597af2bfd9ed90d3e645d91c34b03bf9a commenting out sledgehammer_mtd in Mutabelle diff -r 890fefa597af -r 29e5cae93584 src/HOL/Mutabelle/mutabelle_extra.ML --- a/src/HOL/Mutabelle/mutabelle_extra.ML Mon Dec 06 10:52:45 2010 +0100 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Mon Dec 06 10:52:45 2010 +0100 @@ -24,9 +24,9 @@ val solve_direct_mtd : mtd val try_mtd : mtd - +(* val sledgehammer_mtd : mtd - +*) (* val refute_mtd : mtd val nitpick_mtd : mtd @@ -156,7 +156,7 @@ val try_mtd = ("try", invoke_try) (** sledgehammer **) - +(* fun invoke_sledgehammer thy t = if can (Goal.prove_global thy (Term.add_free_names t []) [] t) (fn {context, ...} => Sledgehammer_Tactics.sledgehammer_with_metis_tac context 1) then @@ -165,7 +165,7 @@ (Unsolved, ([], NONE)) val sledgehammer_mtd = ("sledgehammer", invoke_sledgehammer) - +*) (* fun invoke_refute thy t = let