src/HOL/Mirabelle/Mirabelle_Test.thy
changeset 40634 dc124a486f94
parent 38892 eccc9e2a6412
child 41358 d5e91925916e
     1.1 --- a/src/HOL/Mirabelle/Mirabelle_Test.thy	Mon Nov 22 10:41:53 2010 +0100
     1.2 +++ b/src/HOL/Mirabelle/Mirabelle_Test.thy	Mon Nov 22 10:41:54 2010 +0100
     1.3 @@ -13,6 +13,7 @@
     1.4    "Tools/mirabelle_refute.ML"
     1.5    "Tools/mirabelle_sledgehammer.ML"
     1.6    "Tools/mirabelle_sledgehammer_filter.ML"
     1.7 +  "Tools/sledgehammer_tactic.ML"
     1.8  begin
     1.9  
    1.10  text {*