--- a/src/HOL/IsaMakefile Mon Nov 22 10:41:53 2010 +0100
+++ b/src/HOL/IsaMakefile Mon Nov 22 10:41:54 2010 +0100
@@ -1295,7 +1295,8 @@
Mirabelle/Tools/mirabelle_metis.ML \
Mirabelle/Tools/mirabelle_quickcheck.ML \
Mirabelle/Tools/mirabelle_refute.ML \
- Mirabelle/Tools/mirabelle_sledgehammer.ML
+ Mirabelle/Tools/mirabelle_sledgehammer.ML \
+ Mirabelle/Tools/sledgehammer_tactic.ML
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Mirabelle
--- a/src/HOL/Mirabelle/Mirabelle_Test.thy Mon Nov 22 10:41:53 2010 +0100
+++ b/src/HOL/Mirabelle/Mirabelle_Test.thy Mon Nov 22 10:41:54 2010 +0100
@@ -13,6 +13,7 @@
"Tools/mirabelle_refute.ML"
"Tools/mirabelle_sledgehammer.ML"
"Tools/mirabelle_sledgehammer_filter.ML"
+ "Tools/sledgehammer_tactic.ML"
begin
text {*