# HG changeset patch
# User bulwahn
# Date 1290418914 -3600
# Node ID dc124a486f94e06713352a7bce7b93926f8016a6
# Parent  6cd611ceb64e4bb52e05f0e3d73e27374bb09dc6
adding dependencies to IsaMakefile; adding sledgehammer_tactic in Mirabelle_Test

diff -r 6cd611ceb64e -r dc124a486f94 src/HOL/IsaMakefile
--- 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
 
 
diff -r 6cd611ceb64e -r dc124a486f94 src/HOL/Mirabelle/Mirabelle_Test.thy
--- 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 {*