commenting out sledgehammer_mtd in Mutabelle
authorbulwahn
Mon Dec 06 10:52:45 2010 +0100 (2010-12-06)
changeset 4097429e5cae93584
parent 40973 890fefa597af
child 40975 498f272b4bcb
commenting out sledgehammer_mtd in Mutabelle
src/HOL/Mutabelle/mutabelle_extra.ML
     1.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Dec 06 10:52:45 2010 +0100
     1.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Dec 06 10:52:45 2010 +0100
     1.3 @@ -24,9 +24,9 @@
     1.4  
     1.5  val solve_direct_mtd : mtd
     1.6  val try_mtd : mtd
     1.7 -
     1.8 +(*
     1.9  val sledgehammer_mtd : mtd
    1.10 -
    1.11 +*)
    1.12  (*
    1.13  val refute_mtd : mtd
    1.14  val nitpick_mtd : mtd
    1.15 @@ -156,7 +156,7 @@
    1.16  val try_mtd = ("try", invoke_try)
    1.17  
    1.18  (** sledgehammer **)
    1.19 -
    1.20 +(*
    1.21  fun invoke_sledgehammer thy t =
    1.22    if can (Goal.prove_global thy (Term.add_free_names t [])  [] t)
    1.23        (fn {context, ...} => Sledgehammer_Tactics.sledgehammer_with_metis_tac context 1) then
    1.24 @@ -165,7 +165,7 @@
    1.25      (Unsolved, ([], NONE))
    1.26  
    1.27  val sledgehammer_mtd = ("sledgehammer", invoke_sledgehammer)
    1.28 -
    1.29 +*)
    1.30  (*
    1.31  fun invoke_refute thy t =
    1.32    let